blob: c6b81f543922036a827ed1eff9029272bd821af2 (
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE EmptyCase #-}
module Bug where
import Data.Kind
data Nat = Z | S Nat
data Down :: Nat -> Type where
Down :: !(Down n) -> Down (S n)
data Up :: Nat -> Type where
Up :: !(Up (S n)) -> Up n
f :: Down n -> ()
f (Down r) = ()
f' :: Down (S (S (S (S Z)))) -> ()
f' (Down r) = ()
g :: Up n -> ()
g (Up r) = ()
|
