From 293f739f85459c41c25c28a25c30cc26cc5ea5bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Fri, 13 Dec 2024 19:54:37 +0000
Subject: [PATCH] Remove polymorphism fix up of equations in measEnv

---
 .../src/Language/Haskell/Liquid/Constraint/Init.hs   | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs
index 1f7bace88..4a0e178a9 100644
--- 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