GADT3.hs 532 Bytes
Newer Older
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
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}

-- Panics in bind_args

module GADT3 where

data EQUAL x y where
  EQUAL :: x~y => EQUAL x y

data ZERO
data SUCC n

data Nat n where
  Zero :: Nat ZERO
  Succ :: Nat n -> Nat (SUCC n)

type family PLUS n :: * -> *
type instance PLUS ZERO n = n

plus_zero :: Nat n -> EQUAL (PLUS ZERO n) n
plus_zero Zero = EQUAL
plus_zero (Succ n) = EQUAL

data FOO n where
  FOO_Zero :: FOO ZERO

foo :: Nat m -> Nat n -> FOO n -> FOO (PLUS m n)
foo Zero n s = case plus_zero n of EQUAL -> s