- Definition ξ (wev:WeakExprVar) : LeveledHaskType Γ ★ :=
- match weakTypeToType' φ wev ★ with
- | Error s => fail ("Error in top-level xi: " +++ s)
- | OK t => t @@ nil
+ Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
+ match coreVarToWeakVar cv with
+ | WExprVar wev => match weakTypeToType' φ wev ★ with
+ | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+ | OK t => t @@ nil
+ end
+ | WTypeVar _ => Prelude_error "top-level xi got a type variable"
+ | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"