(fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
; return WECase vscrut' escrut' tbranches' tc tys branches'
- | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+ | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
=> bind tleaf = typeToWeakType (snd vt) ite
; bind v' = mkWeakExprVar tleaf
; return ((fst vt),v'))
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
- match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+ match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
uniqM f => f us >>= fun x => OK (snd x)
end.
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.