Type expected error

Stream: new members

[Josh Cohen]

Hello, I am trying to represent a denotation of polymorphic types in Lean, something like:

inductive ty where
  | int
  | arrow : ty → ty → ty
  | var (s: String)

def to_type (t: ty) (fvs: String → Type) : Type :=
  match t with
  | .int => Int
  | .arrow t1 t2 => to_type t1 fvs → to_type t2 fvs
  | .var s => fvs s

def poly_type (n: Nat) :=
  match n with
  | 0 => Type
  | n' + 1 => Type → poly_type n'

-- Example: to_poly_type ["a", "b"] (.arrow "a" "b") gives (fun (α β : Type), α → β) : Type → Type → Type
def to_poly_type (vars: List String) (t : ty) (acc: String → Type) : poly_type vars.length :=
  match vars with
  | v :: vars => fun (α : Type) => to_poly_type vars t (fun x => if x = v then α else acc x)
  | [] => to_type t acc

structure foo where
  typeVars : List String
  input : ty
  output : ty
  good : to_type (.arrow input output) (fun _ => Empty)
  good2: to_poly_type [] (.arrow input output) (fun _ => Empty)
  bad : to_poly_type typeVars (.arrow input output) (fun _ => Empty)

As the names suggest, bad fails with an error type expected, got (to_poly_type typeVars (input.arrow output) fun x => Empty : poly_type typeVars.length). The monomorphic cases (good and good2) succeed. I am guessing this is because these expressions simplify to something with type Type. However, the polymorphic case simplifies to something with type Type -> ... -> Type. Why is this not allowed, and how could I fix it?

[Aaron Liu]

I don't understand what you actually want to do here

[Josh Cohen]

I want the structure foo to contain a Lean term that has type (denotation of forall typeVars, input -> output). For example, suppose I have typeVars = ["a"], input = .var "a", output = .var "a", I want bad to be a Lean term of type to_poly_type ["a"] (.arrow "a" "a") , which in this case is (fun (α : Type), α → α). An example term of this type would be id. However, I now realize the fun (α : Type) in to_poly_type should be forall (α : Type) and that this approach may not work because of universe inconsistencies.