hadrian: Add support for bindist compressors other than Xz
[ghc.git] / testsuite / tests / typecheck / should_compile / T12466a.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE PolyKinds #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# LANGUAGE TypeOperators #-}
9 module T12466a where
10
11 import GHC.TypeLits (Nat)
12 import Unsafe.Coerce (unsafeCoerce)
13
14 data Dict a where
15 Dict :: a => Dict a
16
17 newtype a :- b = Sub (a => Dict b)
18
19 axiom :: forall a b. Dict (a ~ b)
20 axiom = unsafeCoerce (Dict :: Dict (a ~ a))
21
22 type Divides n m = n ~ Gcd n m
23 type family Gcd :: Nat -> Nat -> Nat where
24
25 dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
26 dividesGcd = Sub axiom