Fix Trac #3102: pre-matching polytypes
authorsimonpj@microsoft.com <unknown>
Mon, 30 Nov 2009 17:44:41 +0000 (17:44 +0000)
committersimonpj@microsoft.com <unknown>
Mon, 30 Nov 2009 17:44:41 +0000 (17:44 +0000)
When *pre-matching* two types
     forall a. C1 => t1  ~  forall a. C2 => t2
we were matching t1~t2, but totally ignoring C1,C2
That's utterly wrong when pre-matching
       (?p::Int) => String  ~  a
because we emerge with a:=String!

All this is part of the impredicative story, which is about
to go away, but still.

Worth merging this to 6.12

compiler/typecheck/TcUnify.lhs

index 7433205..064f199 100644 (file)
@@ -578,9 +578,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
 
     go ty1 ty2          -- C.f. the isSigmaTy case for boxySubMatchType
         | isSigmaTy ty1
-        , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
-        , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+        , (tvs1, ps1, tau1) <- tcSplitSigmaTy ty1
+        , (tvs2, ps2, tau2) <- tcSplitSigmaTy ty2
         , equalLength tvs1 tvs2
+        , equalLength ps1  ps2
         = boxy_match (tmpl_tvs `delVarSetList` tvs1)    tau1
                      (boxy_tvs `extendVarSetList` tvs2) tau2 subst