Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / T14066a.hs
1 {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
2 UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
3
4 module T14066a where
5
6 import Data.Proxy
7 import Data.Kind
8 import Data.Type.Bool
9
10
11 type family Bar x y where
12 Bar (x :: a) (y :: b) = Int
13 Bar (x :: c) (y :: d) = Bool -- a,b,c,d should be SigTvs and unify appropriately
14
15
16 -- the two k's, even though they have different scopes, should unify in the
17 -- kind-check and then work in the type-check because Prox3 has been generalized
18
19 data Prox3 a where
20 MkProx3a :: Prox3 (a :: k1)
21 MkProx3b :: Prox3 (a :: k2)
22
23 -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
24 -- But GHC accepts it because the polymorphic occurrence is at a type variable.
25 data T0 a = forall k (b :: k). MkT0 (T0 b) Int
26
27 -- k and j should unify
28 type family G x a where
29 G Int (b :: k) = Int
30 G Bool (c :: j) = Bool
31
32 -- this last example just checks that GADT pattern-matching on kinds still works.
33 -- nothing new here.
34 data T (a :: k) where
35 MkT :: T (a :: Type -> Type)
36
37 data S (a :: Type -> Type) where
38 MkS :: S a
39
40 f :: forall k (a :: k). Proxy a -> T a -> ()
41 f _ MkT = let y :: S a
42 y = MkS
43 in ()
44
45 -- This is questionable. Should we use the RHS to determine dependency? It works
46 -- now, but if it stops working in the future, that's not a deal-breaker.
47 type P k a = Proxy (a :: k)
48
49
50 -- This is a challenge. It should be accepted, but only because c's kind is learned
51 -- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
52 -- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
53 -- Naively, we don't know about c's kind early enough.
54
55 data SameKind :: forall k. k -> k -> Type
56 type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
57 IfK (_ :: Proxy True) f _ = f
58 IfK (_ :: Proxy False) _ g = g
59 x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
60 x _ = Proxy
61
62
63 f2 :: forall b. b -> Proxy Maybe
64 f2 x = fstOf3 y :: Proxy Maybe
65 where
66 y :: (Proxy a, Proxy c, b)
67 y = (Proxy, Proxy, x)
68
69 fstOf3 (x, _, _) = x
70
71 f3 :: forall b. b -> Proxy Maybe
72 f3 x = fst y :: Proxy Maybe
73 where
74 y :: (Proxy a, b)
75 y = (Proxy, x)
76
77 -- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
78 -- so it is generalized, even with MonoLocalBinds.
79 f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
80 where
81 y :: (Proxy a, Int)
82 y = (Proxy, x)