Clone relevant constraints to avoid side-effects on HoleDests. Fixes #15370.

Summary: When looking for valid hole fits, the constraints relevant
to the hole may sometimes contain a HoleDest. Previously,
these were not cloned, which could cause the filling of filled
coercion hole being, which would cause an assert to fail. This is now fixed.

Test Plan: Regression test included.

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15370

Differential Revision: https://phabricator.haskell.org/D5004

3 files changed, 63 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T15370.hs b/testsuite/tests/typecheck/should_compile/T15370.hs
new file mode 100644
index 0000000000..acccf030bd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15370.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Type.Equality
+
+data S (a :: Either x y)
+
+mkRefl :: n :~: j
+mkRefl = Refl
+
+right :: forall (r :: Either x y).
+         S r -> ()
+right no =
+  case mkRefl @x @y of
+    Refl -> no + _
diff --git a/testsuite/tests/typecheck/should_compile/T15370.stderr b/testsuite/tests/typecheck/should_compile/T15370.stderr
new file mode 100644
index 0000000000..f26cf92c3d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15370.stderr
@@ -0,0 +1,42 @@
+
+T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match type ‘n’ with ‘j’
+      ‘n’ is a rigid type variable bound by
+        the type signature for:
+          mkRefl :: forall k (n :: k) (j :: k). n :~: j
+        at T15370.hs:13:1-17
+      ‘j’ is a rigid type variable bound by
+        the type signature for:
+          mkRefl :: forall k (n :: k) (j :: k). n :~: j
+        at T15370.hs:13:1-17
+      Expected type: n :~: j
+        Actual type: n :~: n
+    • In the expression: Refl
+      In an equation for ‘mkRefl’: mkRefl = Refl
+    • Relevant bindings include
+        mkRefl :: n :~: j (bound at T15370.hs:14:1)
+
+T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match type ‘S r’ with ‘()’
+      Expected type: ()
+        Actual type: S r
+    • In the expression: no + _
+      In a case alternative: Refl -> no + _
+      In the expression: case mkRefl @x @y of { Refl -> no + _ }
+    • Relevant bindings include
+        no :: S r (bound at T15370.hs:18:7)
+        right :: S r -> () (bound at T15370.hs:18:1)
+
+T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
+    • Found hole: _ :: S r
+      Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
+               the type signature for:
+                 right :: forall x y (r :: Either x y). S r -> ()
+               at T15370.hs:(16,1)-(17,18)
+    • In the second argument of ‘(+)’, namely ‘_’
+      In the expression: no + _
+      In a case alternative: Refl -> no + _
+    • Relevant bindings include
+        no :: S r (bound at T15370.hs:18:7)
+        right :: S r -> () (bound at T15370.hs:18:1)
+      Constraints include y ~ x (from T15370.hs:20:5-8)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9d5d7c1b7d..053f9491a7 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -398,6 +398,7 @@ test('abstract_refinement_hole_fits', normal, compile, ['-fdefer-type-errors -fn
 test('free_monad_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -fno-max-refinement-hole-fits -frefinement-level-hole-fits=2 -funclutter-valid-hole-fits'])
 test('constraint_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -fno-max-refinement-hole-fits -frefinement-level-hole-fits=2 -funclutter-valid-hole-fits'])
 test('type_in_type_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits'])
+test('T15370', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -funclutter-valid-hole-fits'])
 test('T7408', normal, compile, [''])
 test('UnboxStrictPrimitiveFields', normal, compile, [''])
 test('T7541', normal, compile, [''])