5b756b2231869e2070bde00f30806e7fc4cff2b7
[ghc.git] / testsuite / tests / typecheck / should_compile / T10009.hs
1 {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
2 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
3 module T10009 where
4
5
6 type family F a
7 type family UnF a
8
9 f :: (UnF (F b) ~ b) => F b -> ()
10 f = error "urk"
11
12 g :: forall a. (UnF (F a) ~ a) => a -> ()
13 g _ = f (undefined :: F a)
14
15
16 {- ---------------
17 [G] UnF (F a) ~ a
18
19 [W] UnF (F beta) ~ beta
20 [W] F a ~ F beta
21
22 -------------------
23 [G] g1: F a ~ fsk1 fsk1 := F a
24 [G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1
25 [G] g3: fsk2 ~ a
26
27 [W] w1: F beta ~ fmv1
28 [W] w2: UnF fmv1 ~ fmv2
29 [W] w3: fmv2 ~ beta
30 [W] w5: fsk1 ~ fmv1 -- From F a ~ F beta
31 -- using flat-cache
32
33 ---- No progress in solving -----
34 -- Unflatten:
35
36 [W] w3: UnF (F beta) ~ beta
37 [W] w5: fsk1 ~ F beta
38
39 --- Improvement
40
41 [D] F beta ~ fmv1
42 [D] UnF fmv1 ~ fmv2 -- (A)
43 [D] fmv2 ~ beta
44 [D] fmv1 ~ fsk1 -- (B) From F a ~ F beta
45 -- NB: put fmv on left
46
47 --> rewrite (A) with (B), and match with g2
48
49 [D] F beta ~ fmv1
50 [D] fmv2 ~ fsk2 -- (C)
51 [D] fmv2 ~ beta -- (D)
52 [D] fmv1 ~ fsk1
53
54 --> rewrite (D) with (C) and re-orient
55
56 [D] F beta ~ fmv1
57 [D] fmv2 ~ fsk2
58 [D] beta ~ fsk2 -- (E)
59 [D] fmv1 ~ fsk1
60
61 -- Now we can unify beta!
62 -}