module Debug

data Unit : U where
  MkUnit : Unit

infixr 7 _::_
data List : U -> U where
  Nil : {A : U} -> List A
  _::_ : {A : U} -> A -> List A -> List A

-- prj/menagerie/papers/combinatory

infixr 6 _~>_
data Type : U where
  ι : Type
  _~>_ : Type -> Type -> Type

A : U
A = Unit

Val : Type -> U
Val ι = A
Val (x ~> y) = Val x -> Val y

-- can't get Val to expand here.
#check (\ x => \ y => \ z => (Val (x ~> y ~> z))) : Type -> Type -> Type -> U

foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> σ))
foo {σ} {τ} {σ} = \ x => \ y => x

