blob: 8f0dbd18782cf30e90cc31f61597c9dac37e415e (
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
27
28
29
|
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE GADTs, ConstraintKinds, TypeFamilies,
DataKinds, ScopedTypeVariables, TypeOperators #-}
module T7090 where
import GHC.Exts
data Dict c where
Dict :: c => Dict c
data Nat = Zero | Succ Nat
type family Plus (a :: Nat) (b :: Nat) :: Nat
type instance Plus Zero b = b
type instance Plus (Succ a) b = Succ (Plus a b)
type One = Succ Zero
type family (a :: Nat) :==: (b :: Nat) :: Bool
boolToProp :: (a :==: b) ~ True => Dict (a ~ b)
boolToProp = undefined
data T (n :: Nat) = MkT
foo :: forall n. (Succ n :==: Plus n One) ~ True => T n
foo = case (boolToProp :: Dict (Succ n ~ Plus n One)) of
Dict -> MkT
|
