Fix polymorphic kvar type variable mismatch and add regression tests

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -289,7 +289,7 @@ buildExprEdges table  = Misc.ordNub . go
     go (PAtom _ e1 e2) = go e1 ++ go e2
     go (ETApp e _)     = go e
     go (ETAbs e _)     = go e
-    go (PKVar _ _)     = []
+    go PKVar{} = []
     go (PExist _ e)    = go e
     go_alias f         = [f | M.member f table ]
 
@@ -654,7 +654,7 @@ expandExpr rtEnv l      = go
     go (PIff    e1 e2)  = PIff       (go e1) (go e2)
     go (PAtom b e1 e2)  = PAtom b    (go e1) (go e2)
     go (EIte  p e1 e2)  = EIte (go p)(go e1) (go e2)
-    go e@(PKVar _ _)    = e
+    go e@PKVar{}        = e
     go e@(ESym _)       = e
     go e@(ECon _)       = e
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -476,8 +476,19 @@ killSubst = fmap killSubstReft
 killSubstReft :: F.Reft -> F.Reft
 killSubstReft = trans ks
   where
-    ks (F.PKVar k _) = F.PKVar k mempty
-    ks p             = p
+    ks (F.PKVar k _ _) = F.PKVar k mempty mempty
+    ks p                = p
+
+-- | Add a type variable → sort mapping to every PKVar in a SpecType.
+-- Used during type application to record how type variables are instantiated,
+-- so the solver can apply the correct sort substitution to qualifier solutions.
+addTyVarSubToKVars :: F.Symbol -> F.Sort -> SpecType -> SpecType
+addTyVarSubToKVars sym sort = fmap (fmap (trans addSub))
+  where
+    addSub (F.PKVar k tsu su) =
+      let tsu' = M.map (F.applyCoercion sym sort) tsu
+       in F.PKVar k (M.insert sym sort tsu') su
+    addSub e                  = e
 
 defAnn :: Bool -> t -> Annot t
 defAnn True  = AnnRDf
@@ -847,7 +858,10 @@ consEApp γ e'@(App e a@(Type τ))
        addW          $ WfC γ t
        t'           <- refreshVV t
        tt0          <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)
-       let tt        = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0
+       let tyVarSym  = F.symbol (ty_var_value α)
+           tyVarSort = typeSort (emb γ) (Ghc.expandTypeSynonyms τ)
+           tt0'      = addTyVarSubToKVars tyVarSym tyVarSort tt0
+           tt        = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0'
        return $ case rTVarToBind α of
          Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)
          Nothing     -> tt

liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs

@@ -847,7 +847,7 @@ substExprV toB su0 = go
     go (PImp p1 p2) = PImp (go p1) (go p2)
     go (PIff p1 p2) = PIff (go p1) (go p2)
     go (PAtom r e1 e2) = PAtom r (go e1) (go e2)
-    go (PKVar k su') = PKVar k $ su' `appendSubst` su0
+    go (PKVar k tsu su') = PKVar k tsu (su' `appendSubst` su0)
     go (PAll _ _) = panic Nothing "substExprV: PAll"
     go (PExist _ _) = panic Nothing "substExprV: PExist"
     go p = p

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Fresh.hs

@@ -56,7 +56,7 @@ instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Symbol w
 instance (Freshable m Integer, Monad m, Applicative m) => Freshable m F.Expr where
   fresh  = kv <$> fresh
     where
-      kv = (`F.PKVar` mempty) . F.intKvar
+      kv i = F.PKVar (F.intKvar i) mempty mempty
 
 instance (Freshable m Integer, Monad m, Applicative m) => Freshable m [F.Expr] where
   fresh = single <$> fresh

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs

@@ -347,7 +347,7 @@ emapExprVM f = go []
       PImp e0 e1 -> PImp <$> go acc e0 <*> go acc e1
       PIff e0 e1 -> PIff <$> go acc e0 <*> go acc e1
       PAtom brel e0 e1 -> PAtom brel <$> go acc e0 <*> go acc e1
-      PKVar k su -> PKVar k <$> emapSubstVM (f . (domain su ++) . (acc ++)) su
+      PKVar k tsu su -> PKVar k tsu <$> emapSubstVM (f . (domain su ++) . (acc ++)) su
       PAll bnds e -> PAll bnds <$> go (map fst bnds ++ acc) e
       PExist bnds e -> PExist bnds <$> go (map fst bnds ++ acc) e
       ECoerc srt0 srt1 e -> ECoerc srt0 srt1 <$> go acc e

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs

@@ -1513,7 +1513,7 @@ appSolRefa si s = mapKVars f0
     mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t
     mapKVars f = trans txK
       where
-        txK (PKVar k su)
+        txK (PKVar k _tsu su)
           | Just p' <- f k =
               rapierSubstExpr (substSymbolsSet $ substFromKSubst su) (renameDomain k su) p'
         txK p = p

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs

@@ -942,11 +942,11 @@ instance F.PPrint KVProf where
 instance NFData KVProf
 
 hole :: F.ExprV v
-hole = F.PKVar "HOLE" (F.toKVarSubst mempty)
+hole = F.PKVar "HOLE" mempty (F.toKVarSubst mempty)
 
 isHole :: Expr -> Bool
-isHole (F.PKVar "HOLE" _) = True
-isHole _                  = False
+isHole (F.PKVar "HOLE" _ _) = True
+isHole _                    = False
 
 hasHole :: (ToReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol) => r -> Bool
 hasHole = any isHole . F.conjuncts . F.reftPred . toReft

tests/ple/neg/PolyKVar2649a.hs

@@ -0,0 +1,23 @@
+{-@ LIQUID "--expect-error-containing=Liquid Type Mismatch" @-}
+{-@ LIQUID "--ple" @-}
+-- | Simple variant of issue #2649: calling a helper with open kvar refinements
+-- from a function that requires a concrete postcondition involving Data.Set.
+-- Previously crashed with a sort mismatch in elaboration.
+module PolyKVar2649a where
+
+import qualified Data.Set as S
+
+{-@ go :: {acc:[a] | _} -> {v:[a] | _ } @-}
+go :: [a] -> [a]
+go xs = xs
+
+{-@ uniques :: (Eq a) => xs:[a] -> {v:ListE a xs | noDups v} @-}
+uniques :: (Eq a) => [a] -> [a]
+uniques xs = go xs
+
+{-@ reflect noDups @-}
+noDups :: (Ord a) => [a] -> Bool
+noDups []     = True
+noDups (x:xs) = noDups xs && not (S.member x (S.fromList xs))
+
+{-@ type ListE a X = {v:[a] | S.listElts v = S.listElts X} @-}

tests/ple/neg/PolyKVar2649b.hs

@@ -0,0 +1,31 @@
+{-@ LIQUID "--expect-error-containing=Liquid Type Mismatch" @-}
+{-@ LIQUID "--ple" @-}
+-- | Original example from issue #2649: polymorphic kvar type variable mismatch
+-- when a local helper function 'go' uses a different type variable than the
+-- outer function 'uniques'. Previously crashed with a sort mismatch in elaboration.
+module PolyKVar2649b (uniques) where
+
+import qualified Data.Set as S
+
+{-@ uniques :: (Eq a) => xs:_ -> {v:ListE a xs | noDups v} @-}
+uniques :: (Eq a) => [a] -> [a]
+uniques xs = go xs []
+  where
+    {-@ go :: (Eq a) => xs:_ -> acc:_ -> {v:ListU a acc xs | _ } @-}
+    go (x:xs) acc
+          | x `isIn` acc = go xs acc
+          | otherwise    = go xs (x:acc)
+    go [] acc        = acc
+
+{-@ isIn :: (Eq a) => x:a -> ys:[a] -> {v:Bool | v = S.member x (S.listElts ys)} @-}
+isIn :: (Eq a) => a -> [a] -> Bool
+isIn _ []     = False
+isIn x (y:ys) = x == y || isIn x ys
+
+{-@ reflect noDups @-}
+noDups :: (Ord a) => [a] -> Bool
+noDups []     = True
+noDups (x:xs) = noDups xs && not (S.member x (S.fromList xs))
+
+{-@ type ListE a X   = {v:[a] | S.listElts v = S.listElts X} @-}
+{-@ type ListU a X Y = {v:[a] | S.listElts v = S.union (S.listElts X) (S.listElts Y)} @-}

tests/ple/pos/PolyKVar2649.hs

@@ -0,0 +1,16 @@
+{-@ LIQUID "--ple" @-}
+module PolyKVar2649 where
+
+-- | A polymorphic helper with kvar-inferred refinements.
+-- The spec says: given input satisfying some kvar, produce output satisfying some kvar.
+-- The implementation is the identity, so the output equals the input.
+{-@ go :: {acc:[a] | _} -> {v:[a] | _ } @-}
+go :: [a] -> [a]
+go xs = xs
+
+-- | A wrapper that calls `go` polymorphically.
+-- The kvars in `go` are instantiated with a different type variable context,
+-- exercising the polymorphic kvar mechanism (issue #2649).
+{-@ wrap :: xs:[a] -> {v:[a] | len v >= 0 } @-}
+wrap :: [a] -> [a]
+wrap xs = go xs

tests/tests.cabal

@@ -2418,6 +2418,7 @@ executable ple-pos
                     , Ple_sum
                     , PolySetFoo
                     , PolySetBar
+                    , PolyKVar2649
                     , ReflectDefault
                     , RegexpDerivative
                     , RosePLEDiv
@@ -2484,6 +2485,8 @@ executable ple-neg
                     , ExactGADT5
                     , Ple0
                     , Ple_sum
+                    , PolyKVar2649a
+                    , PolyKVar2649b
                     , ReflectDefault
                     , T1173
                     , T1192