Skip to content
Browse files

fix for incorrect fix for forall/exists check

  • Loading branch information...
1 parent 3666eda commit 1332129dfd19f5d4a1c9d5ee9705eef22a9cc4f7 @atzedijkstra atzedijkstra committed May 25, 2016
Showing with 16 additions and 5 deletions.
  1. +1 −1 EHC/src/ehc/ConfigInternalVersions.chs
  2. +5 −1 EHC/src/ehc/Ty.cag
  3. +10 −3 EHC/src/ehc/Ty/FitsIn.chs
View
2 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
View
6 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)
View
13 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

0 comments on commit 1332129

Please sign in to comment.
Something went wrong with that request. Please try again.