blob: f630ad5d222578fe8c2ac3705ddfda5eaa202973 (
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
|
{-# 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 m 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
|
