blob: bf3e372461f0ce8dd7e3645bb53c58da5e98fb9a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
{-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators,
TypeFamilies, StarIsType #-}
module DumpRenamedAst where
data Peano = Zero | Succ Peano
type family Length (as :: [k]) :: Peano where
Length (a : as) = Succ (Length as)
Length '[] = Zero
data family Nat :: k -> k -> *
-- Ensure that the `k` in the type pattern and `k` in the kind signature have
-- the same binding site.
newtype instance Nat (a :: k -> *) :: (k -> *) -> * where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
main = putStrLn "hello"
|
