From cfc4fa60de9350533819f29f638c33ed9a91288e Mon Sep 17 00:00:00 2001 From: Ingo Wechsung Date: Sun, 8 Apr 2018 08:02:06 +0200 Subject: [PATCH] corrected unification of generic type vars --- frege/compiler/tc/Util.fr | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/frege/compiler/tc/Util.fr b/frege/compiler/tc/Util.fr index 3c95d68c..957e8d46 100644 --- a/frege/compiler/tc/Util.fr +++ b/frege/compiler/tc/Util.fr @@ -445,12 +445,22 @@ unifyVar ex tv lrtau = do Right tau -> unified ex ty tau Nothing -> either unbound unbound lrtau where - unbound (Meta tv2) + unbound (t2@Meta tv2) + | Just tau1 ← (Meta tv).bounds, Just tau2 ← t2.bounds = do + u ← unified ex tau1 tau2 + when (u) do + writeTv tv t2 + g <- getST + E.logmsg TRACET (getpos ex) (text ("unifyVar: " + ++ show tv.uid ++ " " + ++ tv.nice g + ++ " :: " ++ show tv.kind)) + pure u | Nothing ← KI.unifyKind tv.kind tv2.kind = do g ← getST E.error (getpos ex) (text "Kind error in unification of " - (text (tv.nicer g) <+> text "::" <+> text (show tv.kind) <+> text " with") - (text (tv2.nicer g) <+> text "::" <+> text (show tv2.kind))) + (text (tv.nicer g) <+> text "::" <+> text (tv.kind.nicer g) <+> text " with") + (text (tv2.nicer g) <+> text "::" <+> text (tv2.kind.nicer g))) pure false unbound tau = do -- unifyUnboundVar g <- getST