Remove polymorphism fix up of equations in measEnv

AlecsFerra · Dec 13, 2024 · 293f739 · 293f739
1 parent 8a8eb72
commit 293f739
Showing 1 changed file with 5 additions and 7 deletions.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
@@ -194,7 +194,7 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE
         [ tcb'
         , lts
         , second (rTypeSort tce . val) <$> gsMeas (gsData sp)
-        , [(F.eqName e, eqToPolySort e) | e <- gsImpAxioms (gsRefl sp)]
+        , [(F.eqName e, eqSort e) | e <- gsImpAxioms (gsRefl sp)]
         ]
   , denv     = dmapty val $ gsDicts (gsSig sp)
   , recs     = S.empty
@@ -222,14 +222,12 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE
       lts         = lt1s ++ lt2s
       tcb'        = []
 
--- | Given an equation whose sorts are @FObj "a##..."@, @FObj "b##..."@, etc,
--- replaces those with @FVar@s.
-eqToPolySort :: F.EquationV v -> F.Sort
-eqToPolySort e  =
+-- | Constructs the sort of an equation
+eqSort :: F.EquationV v -> F.Sort
+eqSort e  =
     let s = foldr (F.FFunc . snd) (F.eqSort e) (F.eqArgs e)
         ss = filter (isTyVarName . F.symbolString) $ S.toList $ F.sortSymbols s
-        su = F.mkSortSubst $ zip ss $ map F.FVar [0..]
-     in F.mkPoly (length ss - 1) $ F.sortSubst su s
+     in F.mkPoly (length ss - 1) s
   where
     isTyVarName s = all isLower (take 1 s) && L.isInfixOf "##" s