blob: bea54955182e7ade363a18f8f9b12fdb5e4eb368 (
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
|
{-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
module Test where
data T a where
MkT :: a -> T a
MkT2 :: forall a b. (b ~ T b) => b -> T a
MkT3 :: forall a. (a ~ Bool) => T a
-- Occurs checks in givens
foo :: forall a. (a ~ T a) => a -> a
foo x = x
blah x = case x of
MkT2 y -> ()
-- Mismatches in givens
bloh :: T Int -> ()
bloh x = case x of
MkT3 -> ()
type family F a b
type family G a b
type instance F a Bool = a
type instance G a Char = a
goo1 :: forall a b. (F a b ~ [a]) => b -> a -> a
goo1 = undefined
goo2 :: forall a. G a Char ~ [Int] => a -> a
goo2 = undefined
-- Just an occurs check
test1 = goo1 False undefined
-- A frozen occurs check, now transformed to decomposition error
test2 = goo2 (goo1 False undefined)
test3 = goo1 False (goo2 undefined)
-- A frozen occurs check, now transformed to both a decomposition and occurs check
data M a where
M :: M a
data T2 a b where
T2 :: T2 a b
goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a
goo3 = undefined
goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
goo4 = undefined
test4 = goo4 (goo3 False undefined)
test5 = goo3 False (goo4 undefined)
|
