blob: c192f6a6a50a71fb5b82ee98c136ba156ed43383 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module T14934a where
import Data.Kind (Type)
import GHC.TypeLits
data Foo :: Nat -> Type where
MkFoo0 :: Foo 0
MkFoo1 :: Foo 1
f :: Foo (1 - 0) -> Foo 1
f x = x
g :: Foo (CharToNat '\1') -> Foo 1
g x = x
|
