[commit: ghc] master: Coercible: Unwrap newtypes before coercing under tycons (7e78faf)
git at git.haskell.org
git at git.haskell.org
Tue May 20 08:48:17 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/7e78faf033405bd5f3b6b787343c98e33d767bda/ghc
>---------------------------------------------------------------
commit 7e78faf033405bd5f3b6b787343c98e33d767bda
Author: Joachim Breitner <mail at joachim-breitner.de>
Date: Tue May 20 10:25:26 2014 +0200
Coercible: Unwrap newtypes before coercing under tycons
This fixes parts of #9117.
>---------------------------------------------------------------
7e78faf033405bd5f3b6b787343c98e33d767bda
compiler/typecheck/TcInteract.lhs | 76 ++++++++++++++---------
testsuite/tests/typecheck/should_compile/T9117.hs | 13 ++++
testsuite/tests/typecheck/should_compile/all.T | 1 +
3 files changed, 60 insertions(+), 30 deletions(-)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a6b7f44..fc8466b 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1929,6 +1929,8 @@ getCoercibleInst loc ty1 ty2 = do
where
go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
go famenv rdr_env
+ -- Also see [Order of Coercible Instances]
+
-- Coercible a a (see case 1 in [Coercible Instances])
| ty1 `tcEqType` ty2
= do return $ GenInst []
@@ -1944,7 +1946,19 @@ getCoercibleInst loc ty1 ty2 = do
ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
return $ GenInst [] ev_term
- -- Coercible (D ty1 ty2) (D ty1' ty2') (see case 3 in [Coercible Instances])
+ -- Coercible NT a (see case 4 in [Coercible Instances])
+ | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
+ Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
+ dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
+ = do markDataConsAsUsed rdr_env tc
+ ct_ev <- requestCoercible loc concTy ty2
+ local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2
+ let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
+ tcCo = TcLetCo binds $
+ coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var
+ return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
+
+ -- Coercible (D ty1 ty2) (D ty1' ty2') (see case 2 in [Coercible Instances])
| Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
tc1 == tc2,
@@ -1975,19 +1989,7 @@ getCoercibleInst loc ty1 ty2 = do
tcCo = TcLetCo binds (mkTcTyConAppCo Representational tc1 arg_cos)
return $ GenInst (catMaybes arg_new) (EvCoercion tcCo)
- -- Coercible NT a (see case 4 in [Coercible Instances])
- | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
- Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
- dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
- = do markDataConsAsUsed rdr_env tc
- ct_ev <- requestCoercible loc concTy ty2
- local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2
- let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
- tcCo = TcLetCo binds $
- coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var
- return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
-
- -- Coercible a NT (see case 4 in [Coercible Instances])
+ -- Coercible a NT (see case 3 in [Coercible Instances])
| Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
@@ -2047,26 +2049,14 @@ air, in getCoercibleInst. The following “instances” are present:
(which would be illegal to write like that in the source code, but we have
it nevertheless).
-
- 3. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
- Coercible (C t1_r t2_r ... t1_p t2_p ... t1_n t2_n ...)
- (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
- for a type constructor C where
- * the nominal type arguments are not changed,
- * the phantom type arguments may change arbitrarily
- * the representational type arguments are again Coercible
-
- The type constructor can be used undersaturated; then the Coercible
- instance is at a higher kind. This does not cause problems.
-
- 4. instance Coercible r b => Coercible (NT t1 t2 ...) b
+ 3. instance Coercible r b => Coercible (NT t1 t2 ...) b
instance Coercible a r => Coercible a (NT t1 t2 ...)
for a newtype constructor NT (or data family instance that resolves to a
newtype) where
* r is the concrete type of NT, instantiated with the arguments t1 t2 ...
* the constructor of NT are in scope.
- Again, the newtype TyCon can appear undersaturated, but only if it has
+ The newtype TyCon can appear undersaturated, but only if it has
enough arguments to apply the newtype coercion (which is eta-reduced). Examples:
newtype NT a = NT (Either a Int)
Coercible (NT Int) (Either Int Int) -- ok
@@ -2074,12 +2064,24 @@ air, in getCoercibleInst. The following “instances” are present:
newtype NT3 a b = NT3 (b -> a)
Coercible (NT2 Int) (NT3 Int) -- cannot be derived
+ 4. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
+ Coercible (C t1_r t2_r ... t1_p t2_p ... t1_n t2_n ...)
+ (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
+ for a type constructor C where
+ * the nominal type arguments are not changed,
+ * the phantom type arguments may change arbitrarily
+ * the representational type arguments are again Coercible
+
+ The type constructor can be used undersaturated; then the Coercible
+ instance is at a higher kind. This does not cause problems.
+
+
The type checker generates evidence in the form of EvCoercion, but the
TcCoercion therein has role Representational, which are turned into Core
coercions by dsEvTerm in DsBinds.
-The evidence for the first three instance is generated here by
-getCoercibleInst, for the second instance deferTcSForAllEq is used.
+The evindence for the second case is created by deferTcSForAllEq, for the other
+cases by getCoercibleInst.
When the constraint cannot be solved, it is treated as any other unsolved
constraint, i.e. it can turn up in an inferred type signature, or reported to
@@ -2088,6 +2090,20 @@ coercible_msg in TcErrors gives additional explanations of why GHC could not
find a Coercible instance, so it duplicates some of the logic from
getCoercibleInst (in negated form).
+Note [Order of Coercible Instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+At first glance, the order of the various coercible instance doesn't matter, as
+incoherence is no issue here: We do not care how the evidence is constructed,
+as long as it is.
+
+But since the solver does not backtrack, the order does matter, as otherwise we may run
+into dead ends. If case 4 (coercing under type constructors) were tried before
+case 3 (unwrapping newtypes), which is tempting, as it yields solutions faster
+and builds smaller evidence turns, then using a role annotation this can
+prevent the solver from finding an otherwise possible solution. See T9117.hs
+for the code.
+
Note [Instance and Given overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/typecheck/should_compile/T9117.hs b/testsuite/tests/typecheck/should_compile/T9117.hs
new file mode 100644
index 0000000..cb05bf2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T9117.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE RoleAnnotations #-}
+
+-- Also see Note [Order of Coercible Instances]
+
+module T9117 where
+
+import Data.Coerce
+
+newtype Phant a = MkPhant Char
+type role Phant representational
+
+ex1 :: Phant Bool
+ex1 = coerce (MkPhant 'x' :: Phant Int)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 373e739..2c3efad 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -418,3 +418,4 @@ test('T8644', normal, compile, [''])
test('T8762', normal, compile, [''])
test('MutRec', normal, compile, [''])
test('T8856', normal, compile, [''])
+test('T9117', normal, compile, [''])
More information about the ghc-commits
mailing list