| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
-(* the WeakType argument in WEBrak/WEEsc is used only when going back *)
-(* from Weak to Core; it lets us dodge a possibly-failing type *)
-(* calculation *)
-| WEBrak : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
-| WEEsc : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
+(* The WeakType argument in WEBrak/WEEsc is used only when going back *)
+(* from Weak to Core; it lets us dodge a possibly-failing type *)
+(* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *)
+(* or hetmet_esc identifier *)
+| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
+| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
-(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
-| WECase : forall (scrutinee:WeakExpr)
+| WECase : forall (vscrut:WeakExprVar)
+ (scrutinee:WeakExpr)
(tbranches:WeakType)
(tc:TyCon)
(type_params:list WeakType)
end
| WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
| WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
- | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
+ | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
| WELet ev ve e => weakTypeOfWeakExpr e
| WELetRec rb e => weakTypeOfWeakExpr e
| WENote n e => weakTypeOfWeakExpr e
- | WECast e (weakCoercion t1 t2 _) => OK t2
- | WECase scrutinee tbranches tc type_params alts => OK tbranches
+ | WECast e (weakCoercion _ t1 t2 _) => OK t2
+ | WECase vscrut scrutinee tbranches tc type_params alts => OK tbranches
(* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
- | WEBrak ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
- | WEEsc ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
+ | WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
+ | WEEsc _ ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
match t' with
| (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
if eqd_dec ec ec' then OK t''