summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_compile/T14066a.hs
blob: 30b203d31b22b0d7e798daa20a92341c53543468 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
             UndecidableInstances, RankNTypes, ScopedTypeVariables #-}

module T14066a where

import Data.Proxy
import Data.Kind
import Data.Type.Bool


type family Bar x y where
  Bar (x :: a) (y :: b) = Int
  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be SigTvs and unify appropriately


  -- the two k's, even though they have different scopes, should unify in the
  -- kind-check and then work in the type-check because Prox3 has been generalized

data Prox3 a where
  MkProx3a :: Prox3 (a :: k1)
  MkProx3b :: Prox3 (a :: k2)

  -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
  -- But GHC accepts it because the polymorphic occurrence is at a type variable.
data T0 a = forall k (b :: k). MkT0 (T0 b) Int

  -- k and j should unify
type family G x a where
  G Int (b :: k) = Int
  G Bool (c :: j) = Bool

-- this last example just checks that GADT pattern-matching on kinds still works.
-- nothing new here.
data T (a :: k) where
  MkT :: T (a :: Type -> Type)

data S (a :: Type -> Type) where
  MkS :: S a

f :: forall k (a :: k). Proxy a -> T a -> ()
f _ MkT = let y :: S a
              y = MkS
          in ()

-- This is questionable. Should we use the RHS to determine dependency? It works
-- now, but if it stops working in the future, that's not a deal-breaker.
type P k a = Proxy (a :: k)


-- This is a challenge. It should be accepted, but only because c's kind is learned
-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
-- Naively, we don't know about c's kind early enough.

data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
   IfK (_ :: Proxy True)  f _ = f
   IfK (_ :: Proxy False) _ g = g
x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
x _ = Proxy


f2 :: forall b. b -> Proxy Maybe
f2 x = fstOf3 y :: Proxy Maybe
  where
    y :: (Proxy a, Proxy c, b)
    y = (Proxy, Proxy, x)

fstOf3 (x, _, _) = x

f3 :: forall b. b -> Proxy Maybe
f3 x = fst y :: Proxy Maybe
  where
    y :: (Proxy a, b)
    y = (Proxy, x)

-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
-- so it is generalized, even with MonoLocalBinds.
f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
  where
    y :: (Proxy a, Int)
    y = (Proxy, x)