Re-engineer Given flatten-skolems
[ghc.git] / testsuite / tests / indexed-types / should_fail / T13674.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE PolyKinds #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeApplications #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE TypeOperators #-}
10
11 module T13674 where
12
13 import Data.Proxy
14 import GHC.Exts (Constraint)
15 import GHC.TypeLits
16 import Unsafe.Coerce (unsafeCoerce)
17
18 data Dict :: Constraint -> * where
19 Dict :: a => Dict a
20
21 infixr 9 :-
22 newtype a :- b = Sub (a => Dict b)
23
24 -- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
25 (\\) :: a => (b => r) -> (a :- b) -> r
26 r \\ Sub Dict = r
27
28 newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
29
30 magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
31 magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
32
33 type family Lcm :: Nat -> Nat -> Nat where
34
35 axiom :: forall a b. Dict (a ~ b)
36 axiom = unsafeCoerce (Dict :: Dict (a ~ a))
37
38 lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
39 lcmNat = magic lcm
40
41 lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
42 lcmIsIdempotent = axiom
43
44 newtype GF (n :: Nat) = GF Integer
45
46 x :: GF 5
47 x = GF 3
48
49 y :: GF 5
50 y = GF 4
51
52 foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
53 foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
54
55 bar :: (KnownNat m) => GF m -> GF m -> GF m
56 bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)