Introduce GHC.TypeNats module, change KnownNat evidence to be Natural
[ghc.git] / testsuite / tests / typecheck / should_fail / ContextStack2.hs
1 {-# LANGUAGE AllowAmbiguousTypes, TypeFamilies #-}
2
3 module ContextStack2 where
4
5 type family TF a :: *
6 type instance TF (a,b) = (TF a, TF b)
7
8 -- Succeeds with new approach to fuvs
9 -- Aug 2016
10 t :: (a ~ TF (a,Int)) => Int
11 t = undefined
12
13 {- a ~ TF (a,Int)
14 ~ (TF a, TF Int)
15 ~ (TF (TF (a,Int)), TF Int)
16 ~ (TF (TF a, TF Int), TF Int)
17 ~ ((TF (TF a), TF (TF Int)), TF Int)
18
19
20 fsk ~ a
21 TF (a, Int) ~ fsk
22 -->
23 fsk ~ a
24 * fsk ~ (TF a, TF Int)
25 (flatten lhs)
26 a ~ (TF a, TF Int)
27 (flatten rhs)
28 a ~ (fsk1, TF Int)
29 (wk) TF a ~ fsk1
30
31 --> (rewrite inert)
32
33 fsk ~ (fsk1, TF Int)
34 a ~ (fsk1, TF Int)
35 (wk) TF a ~ fsk1
36
37 -->
38 fsk ~ (fsk1, TF Int)
39 a ~ (fsk1, TF Int)
40
41 * TF (fsk1, fsk2) ~ fsk1
42 (wk) TF Tnt ~ fsk2
43
44 -->
45 fsk ~ (fsk1, TF Int)
46 a ~ (fsk1, TF Int)
47
48 * fsk1 ~ (TF fsk1, TF fsk2)
49 (flatten rhs)
50 fsk1 ~ (fsk3, TF fsk2)
51
52
53 (wk) TF Int ~ fsk2
54 TF fsk1 ~ fsk3
55 -}