Stop marking soluble ~R# constraints as insoluble
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 23 Jul 2018 14:33:13 +0000 (15:33 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 23 Jul 2018 14:53:34 +0000 (15:53 +0100)
We had a constraint (a b ~R# Int), and were marking it as 'insoluble'.
That's bad; it isn't.  And it caused Trac #15431. Soultion is simple.

I did a tiny refactor on can_eq_app, so that it is used only for
nominal equalities.

compiler/typecheck/TcCanonical.hs
testsuite/tests/typecheck/should_compile/T15431.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T15431a.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 42f28c7..c45afd2 100644 (file)
@@ -894,11 +894,13 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
 
 -- See Note [Canonicalising type applications] about why we require flat types
 can_eq_nc' True _rdr_env _envs ev eq_rel (AppTy t1 s1) _ ty2 _
-  | Just (t2, s2) <- tcSplitAppTy_maybe ty2
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t2, s2) <- tcSplitAppTy_maybe ty2
+  = can_eq_app ev t1 s1 t2 s2
 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
-  | Just (t1, s1) <- tcSplitAppTy_maybe ty1
-  = can_eq_app ev eq_rel t1 s1 t2 s2
+  | NomEq <- eq_rel
+  , Just (t1, s1) <- tcSplitAppTy_maybe ty1
+  = can_eq_app ev t1 s1 t2 s2
 
 -- No similarity in type structure detected. Flatten and try again.
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
@@ -908,9 +910,22 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
        ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
 -- We've flattened and the types don't match. Give up.
-can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
-       ; canEqHardFailure ev ps_ty1 ps_ty2 }
+       ; case eq_rel of -- See Note [Unsolved equalities]
+            ReprEq -> continueWith (mkIrredCt ev)
+            NomEq  -> continueWith (mkInsolubleCt ev) }
+          -- No need to call canEqFailure/canEqHardFailure because they
+          -- flatten, and the types involved here are already flat
+
+{- Note [Unsolved equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have an unsolved equality like
+  (a b ~R# Int)
+that is not necessarily insoluble!  Maybe 'a' will turn out to be a newtype.
+So we want to make it a potentially-soluble Irred not an insoluble one.
+Missing this point is what caused Trac #15431
+-}
 
 ---------------------------------
 can_eq_nc_forall :: CtEvidence -> EqRel
@@ -1220,8 +1235,8 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
 ---------
 -- ^ Decompose a type application.
 -- All input types must be flat. See Note [Canonicalising type applications]
-can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
-           -> EqRel            -- r
+-- Nominal equality only!
+can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
            -> Xi -> Xi         -- s1 t1
            -> Xi -> Xi         -- s2 t2
            -> TcS (StopOrContinue Ct)
@@ -1229,13 +1244,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 -- AppTys only decompose for nominal equality, so this case just leads
 -- to an irreducible constraint; see typecheck/should_compile/T10494
 -- See Note [Decomposing equality], note {4}
-can_eq_app ev ReprEq _ _ _ _
-  = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
-       ; continueWith (mkIrredCt ev) }
-          -- no need to call canEqFailure, because that flattens, and the
-          -- types involved here are already flat
-
-can_eq_app ev NomEq s1 t1 s2 t2
+can_eq_app ev s1 t1 s2 t2
   | CtDerived { ctev_loc = loc } <- ev
   = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
        ; stopWith ev "Decomposed [D] AppTy" }
diff --git a/testsuite/tests/typecheck/should_compile/T15431.hs b/testsuite/tests/typecheck/should_compile/T15431.hs
new file mode 100644 (file)
index 0000000..21fa4c4
--- /dev/null
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs, FlexibleContexts #-}
+
+module T15431 where
+
+import Data.Coerce
+
+data T t where
+  A :: Show (t a) => t a -> T t
+  B :: Coercible Int (t a) => t a -> T t
+
+f :: T t -> String
+f (A t) = show t
+
+g :: T t -> Int
+g (B t) = coerce t
diff --git a/testsuite/tests/typecheck/should_compile/T15431a.hs b/testsuite/tests/typecheck/should_compile/T15431a.hs
new file mode 100644 (file)
index 0000000..cf5a831
--- /dev/null
@@ -0,0 +1,12 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+module T15431a where
+
+import Data.Coerce
+import Data.Functor.Identity
+
+g1 :: Coercible (t a) Int => t a -> Int
+g1 = coerce
+
+g2 :: Coercible Int (t a) => t a -> Int
+g2 = coerce
index 10295f5..6babe4e 100644 (file)
@@ -640,3 +640,5 @@ def onlyHsParLocs(x):
                         and not "<no location info>" in loc)
     return '\n'.join(filteredLines)
 test('T15242', normalise_errmsg_fun(onlyHsParLocs), compile, [''])
+test('T15431', normal, compile, [''])
+test('T15431a', normal, compile, [''])