blob: 4905989ead391c6767a419d7bae598fb14d01b6b (
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
30
31
32
33
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data Nat = Z | S Nat
data SNat :: Nat -> Type where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family S' (n :: Nat) :: Nat where
S' n = S n
data R :: Nat -> Nat -> Nat -> Type where
MkR :: !(R m n o) -> R (S m) n (S o)
type family NatPlus (m :: Nat) (n :: Nat) :: Nat where
NatPlus Z n = n
NatPlus (S m) n = S' (NatPlus m n)
f :: forall (m :: Nat) (n :: Nat) (o :: Nat).
SNat m -> SNat n -> SNat o
-> R m n o -> NatPlus m n :~: o
f (SS sm) sn (SS so) (MkR r)
| Refl <- f sm sn so r
= Refl
|
