fix for incorrect fix for forall/exists check

Author: atzedijkstra

EHC/src/ehc/ConfigInternalVersions.chs

@@ -35,7 +35,7 @@ internalVersionCombined =
 
 %%[50 hs export(internalVersionTySys, internalVersionCodeGen, internalVersionHI, internalVersionCore, internalVersionCoreRun, internalVersionHS)
 -- | For variation in type inferencing
-internalVersionTySys = mkInternalVersion 1
+internalVersionTySys = mkInternalVersion 2
 
 -- | For variation in code gen
 internalVersionCodeGen = mkInternalVersion 1

EHC/src/ehc/Ty.cag

@@ -551,7 +551,7 @@ tyQu_KiExists = TyQu_Exists metaLevTy
 %%% Properties of quantifier
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%[(4 hmtyinfer || hmtyast) hs export(tyquIsExists, tyquIsForall)
+%%[(4 hmtyinfer || hmtyast) hs export(tyquEqModuloLev, tyquIsExists, tyquIsForall)
 tyquIsExists, tyquIsForall :: TyQu -> Bool
 %%]
 
@@ -561,6 +561,10 @@ tyquIsForall _                       = False
 
 tyquIsExists (TyQu_Exists _)         = True
 tyquIsExists _                       = False
+
+tyquEqModuloLev (TyQu_Forall {}) (TyQu_Forall {}) = True
+tyquEqModuloLev (TyQu_Exists {}) (TyQu_Exists {}) = True
+tyquEqModuloLev _                _                = False
 %%]
 
 %%[(4 hmtyinfer || hmtyast) hs export(tyquMetaLev)

EHC/src/ehc/Ty/FitsIn.chs

@@ -461,6 +461,13 @@ fitsInFI fi ty1 ty2
                        (uqt,rtvs,instto) = tyInst1Quants uq howToInst t
                        back              = if hide  then  \fo -> foSetVarMp (varmpDel rtvs (foVarMp fo)) $ foUpdTy t fo
                                                     else  id
+
+            -- removal of multiple quantifiers
+            unquants fi t@(Ty_TBind {qu_Ty_TBind=q}) qu howToInst | qu `tyquEqModuloLev` q
+                = unquants fi' t' qu howToInst
+                where (fi', t', _, _) = unquant fi t False howToInst
+            unquants fi t _ _
+                = (fi, t)
 %%]
 
 %%[(41 hmtyinfer).fitsIn.eqProofAssume
@@ -1191,12 +1198,12 @@ GADT: when encountering a product with eq-constraints on the outset, remove them
 %%[(4 hmtyinfer).fitsIn.QLR
             fBase fi updTy t1@(Ty_TBind {qu_Ty_TBind=q1})   t2@(Ty_TBind {qu_Ty_TBind=q2})
                 | fiom `elem` [FitSubLR,FitUnify]
-                                                    = if q1 == q2 
+                                                    = if q1 `tyquEqModuloLev` q2 
                                                       then fVar' fTySyn fi2 id uqt1 uqt2
                                                       else errClash fi t1 t2
                 where  fiom = fioMode (fiFIOpts fi)
-                       (fi1,uqt1,_,_) = unquant fi   t1 False instCoConst
-                       (fi2,uqt2,_,_) = unquant fi1  t2 False (if fiom == FitSubLR then instContra else instCoConst)
+                       (fi1,uqt1) = unquants fi   t1 q1 instCoConst
+                       (fi2,uqt2) = unquants fi1  t2 q1 (if fiom == FitSubLR then instContra else instCoConst)
 %%]
 
 %%[(4 hmtyinfer).fitsIn.QR