Pmc: Treat `x ~ y @ty` the same as `x ~ y` (#23145)wip/T23145

In #23145 we had a desugaring that matched on expressions `ds @Any`
and `ds @blah` (where `blah /= Any`). In both cases, we match on the
same value, but Long-distance information was unable to figure this
out.

The fix is rather simple: Upon reasoning about the Core constraint
`x ~ ds @Any`, drop any type arguments to see `x ~ ds`, then we will
equate that to the same as `ds @blah`.

This plays a bit fast-and-loose with types; on the other hand, the
situations in which can give the same value different types should
be exceedingly rare.

Fixes #23145.

3 files changed, 58 insertions, 6 deletions

diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index b493d41889..9337a9e7cf 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -868,15 +868,23 @@ addCoreCt nabla x e = do
           -- Otherwise we alternate endlessly between [] and ""
           [] -> data_con_app x emptyInScopeSet nilDataCon []
           s' -> core_expr x (mkListExpr charTy (map mkCharExpr s'))
+
       | Just lit <- coreExprAsPmLit e
       = pm_lit x lit
+
       | Just (in_scope, _empty_floats@[], dc, _arg_tys, args)
             <- exprIsConApp_maybe in_scope_env e
       = data_con_app x in_scope dc args
-      -- See Note [Detecting pattern synonym applications in expressions]
-      | Var y <- e, Nothing <- isDataConId_maybe x
-      -- We don't consider DataCons flexible variables
+          -- See Note [Detecting pattern synonym applications in expressions]
+
+      | (Var y, args) <- collectArgs e
+          -- This catches the case of a variable constraints `x ~ y`
+      , all isTypeArg args
+          -- See Note [Identify VarInfo modulo type arguments]
+      , Nothing <- isDataConId_maybe x
+          -- We don't consider DataCons flexible variables
       = modifyT (\nabla -> addVarCt nabla x y)
+
       | otherwise
       -- Any other expression. Try to find other uses of a semantically
       -- equivalent expression and represent them by the same variable!
@@ -1059,10 +1067,41 @@ In the end, replacing dictionaries with an error value in the pattern-match
 checker was the most self-contained, although we might want to revisit once
 we implement a more robust approach to computing equality in the pattern-match
 checker (see #19272).
--}
 
-{- Note [The Pos/Neg invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Identify VarInfo modulo type arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#23145)
+
+  f :: (forall a. Maybe a) -> Maybe b
+  f (Just x) = Just x
+  f Nothing  = Nothing
+
+this desugars to
+
+  f = \ @b (ds :: forall a. Maybe a) ->
+        case ds @b of {
+          Just x  -> Just @b x;
+          Nothing ->
+            case ds @Any of {
+              Just ipv -> patError ...
+              Nothing -> Nothing @b
+            }
+        }
+
+Note we match on `ds` twice with different type arguments applied, but since the
+type arguments are erased both matches must yield the same value. Hence we should
+not warn about `f` having an incomplete match.
+A good way to achieve that is discard the type arguments in the constraint `pm
+~ ds @b` (where `pm` is the match variable of the outermost Case) so that we
+get `pm ~ ds`, with the outcome of giving both match variables the same VarInfo
+as `ds`. Long distance information will sort out the rest and we the checker
+detects `f` as exhaustive.
+
+Note that the potential type confusion is harmless as the TyCon of `ds` and `pm`
+must be the same (if it exists).
+
+Note [The Pos/Neg invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Invariant applying to each VarInfo: Whenever we have @C @tvs args@ in 'vi_pos',
 any entry in 'vi_neg' must be incomparable to C (return Nothing) according to
 'eqPmAltCons'. Those entries that are comparable either lead to a refutation
diff --git a/testsuite/tests/pmcheck/should_compile/T23145.hs b/testsuite/tests/pmcheck/should_compile/T23145.hs
new file mode 100644
index 0000000000..a792fb7e27
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T23145.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module T23145 where
+
+data T a
+  = MkT1 a
+  | MkT2
+
+f :: (forall a. T a) -> T b
+f (MkT1 x) = MkT1 x
+f MkT2 = MkT2
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 94c044b3d8..b9153e39b9 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -159,3 +159,4 @@ test('EmptyCase010', [],  compile, [overlapping_incomplete])
 test('T19271', [],  compile, [overlapping_incomplete])
 test('T21761', [],  compile, [overlapping_incomplete])
 test('T22964', [], compile, [overlapping_incomplete])
+test('T23145', [], compile, [overlapping_incomplete])