corrected unification of generic type vars

Frege · Apr 8, 2018 · cfc4fa6 · cfc4fa6
1 parent 992b70b
commit cfc4fa6
Showing 1 changed file with 13 additions and 3 deletions.
diff --git 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