Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T7090.hs
1 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
2 {-# LANGUAGE GADTs, ConstraintKinds, TypeFamilies,
3 DataKinds, ScopedTypeVariables, TypeOperators #-}
4
5 module T7090 where
6
7 import GHC.Exts
8
9 data Dict c where
10 Dict :: c => Dict c
11
12 data Nat = Zero | Succ Nat
13
14 type family Plus (a :: Nat) (b :: Nat) :: Nat
15 type instance Plus Zero b = b
16 type instance Plus (Succ a) b = Succ (Plus a b)
17
18 type One = Succ Zero
19
20 type family (a :: Nat) :==: (b :: Nat) :: Bool
21
22 boolToProp :: (a :==: b) ~ True => Dict (a ~ b)
23 boolToProp = undefined
24
25 data T (n :: Nat) = MkT
26
27 foo :: forall n. (Succ n :==: Plus n One) ~ True => T n
28 foo = case (boolToProp :: Dict (Succ n ~ Plus n One)) of
29 Dict -> MkT