blob: 7761eafe97d37068ff1a684ff2b441aa16da7e1e (
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
|
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
-- This wrongly fails with
--
-- Can't construct the infinite type n = PLUS n ZERO
module GADT1 where
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
type instance PLUS (SUCC m) n = SUCC (PLUS m n)
data EQUIV x y where
EQUIV :: EQUIV x x
plus_zero :: Nat n -> EQUIV (PLUS n ZERO) n
plus_zero Zero = EQUIV
plus_zero (Succ n) = case plus_zero n of
EQUIV -> EQUIV
|
