From 0c88b710a0ac7fc20363527ff88224b221ff923d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Mon, 2 Dec 2024 21:39:56 +0000 Subject: [PATCH] Fix detection of tyvars when generalizing sorts of gsImpAxioms --- .../src/Language/Haskell/Liquid/Constraint/Init.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs index 0043621a9..1f7bace88 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -222,14 +222,16 @@ 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, +-- | Given an equation whose sorts are @FObj "a##..."@, @FObj "b##..."@, etc, -- replaces those with @FVar@s. eqToPolySort :: F.EquationV v -> F.Sort eqToPolySort e = let s = foldr (F.FFunc . snd) (F.eqSort e) (F.eqArgs e) - ss = filter (all isLower . take 1 . F.symbolString) $ S.toList $ F.sortSymbols s + 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 + where + isTyVarName s = all isLower (take 1 s) && L.isInfixOf "##" s assm :: TargetInfo -> [(Var, SpecType)] assm = assmGrty (giImpVars . giSrc)