c26a1846890bf53e273c81502509b733e3055539
[ghc.git] / testsuite / tests / dependent / should_compile / T14720.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE TypeInType #-}
7 {-# LANGUAGE TypeOperators #-}
8 module T14720 where
9
10 import Data.Kind (Type)
11 import Data.Type.Equality ((:~:)(..), sym, trans)
12 import Data.Void
13
14 data family Sing (z :: k)
15
16 class Generic (a :: Type) where
17 type Rep a :: Type
18 from :: a -> Rep a
19 to :: Rep a -> a
20
21 class PGeneric (a :: Type) where
22 type PFrom (x :: a) :: Rep a
23 type PTo (x :: Rep a) :: a
24
25 class SGeneric k where
26 sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
27 sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
28
29 class (PGeneric k, SGeneric k) => VGeneric k where
30 sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
31 sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
32
33 data Decision a = Proved a
34 | Disproved (a -> Void)
35
36 class SDecide k where
37 (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
38 default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
39 => Sing a -> Sing b -> Decision (a :~: b)
40 s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
41 Proved (Refl :: PFrom a :~: PFrom b) ->
42 case (sTof s1, sTof s2) of
43 (Refl, Refl) -> Proved Refl
44 Disproved contra -> Disproved (\Refl -> contra Refl)