Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T11249.hs
1 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies,
2 KindSignatures, ConstraintKinds #-}
3
4 module T11249 where
5
6 import GHC.TypeLits
7
8 type a / b = FDiv a b
9 type a ** b = FMul a b
10
11 type family FDiv a b where
12 FDiv 11648 128 = 91
13
14 type family FMul a b where
15 FMul 64 91 = 5824
16
17 type family FGCD a b where
18 FGCD 128 448 = 64
19 FGCD 128 5824 = 64
20
21 type family FLCM a b where
22 FLCM 128 5824 = 11648
23
24 data CT (m :: Nat) (m' :: Nat)
25 type H0 = 128
26 type H1 = 448
27 type H0' = 11648
28 type H1' = 5824
29
30 main' = let x = undefined :: CT H0 H0'
31 in foo x :: CT H1 H1'
32
33 foo x = bug x
34
35 type Ctx2 e r s e' r' =
36 (e ~ FGCD r e', r' ~ FLCM r e', e ~ FGCD r s)
37
38 bug :: (Ctx2 e r s e' r', e' ~ (e ** (FDiv r' r)))
39 => CT r r' -> CT s s'
40 bug = undefined