Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / typecheck / should_compile / T12919.hs
1 {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, ConstraintKinds #-}
2
3 module T12919 where
4
5 import Data.Kind
6
7 data N = Z
8
9 data V :: N -> Type where
10 VZ :: V Z
11
12 type family VC (n :: N) :: Type where
13 VC Z = Type
14
15 type family VF (xs :: V n) (f :: VC n) :: Type where
16 VF VZ f = f
17
18 data Dict c where
19 Dict :: c => Dict c
20
21 prop :: xs ~ VZ => Dict (VF xs f ~ f)
22 prop = Dict