(*
Require Import HaskStrongCategory.
*)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
Open Scope string_scope.
Extraction Language Haskell.
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
| WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
- | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+ | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
+ toString cv+++": " +++ s)
| OK t => t @@ nil
end
| WTypeVar _ => Prelude_error "top-level xi got a type variable"