blob: d0749e6b0af88a67af02be8deb1aa72745232882 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T12466a where
import GHC.TypeLits (Nat)
import Unsafe.Coerce (unsafeCoerce)
data Dict a where
Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))
type Divides n m = n ~ Gcd n m
type family Gcd :: Nat -> Nat -> Nat where
dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesGcd = Sub axiom
|
