Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T8705.hs
1 {-# LANGUAGE TypeOperators, DataKinds, PolyKinds,
2 MultiParamTypeClasses, GADTs, ConstraintKinds, TypeFamilies #-}
3 module T8705 where
4
5 data family Sing (a :: k)
6 data Proxy a = Proxy
7
8 data instance Sing (a :: Maybe k) where
9 SJust :: Sing h -> Sing (Just h)
10
11 data Dict c where
12 Dict :: c => Dict c
13
14 -- A less-than-or-equal relation among naturals
15 class a :<=: b
16
17 sLeq :: Sing n -> Sing n2 -> Dict (n :<=: n2)
18 sLeq = undefined
19
20 insert_ascending :: (lst ~ Just n1) => Proxy n1 -> Sing n -> Sing lst -> Dict (n :<=: n1)
21 insert_ascending _ n (SJust h)
22 = case sLeq n h of
23 Dict -> Dict