[commit: ghc] master: Improve Note [Order of Coercible Instances] about Trac #9117 (9e10963)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/9e10963e394680dbb1b964c66cb428a2aa03df09/ghc

>---------------------------------------------------------------

commit 9e10963e394680dbb1b964c66cb428a2aa03df09
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri May 30 10:25:21 2014 +0100

    Improve Note [Order of Coercible Instances] about Trac #9117


>---------------------------------------------------------------

9e10963e394680dbb1b964c66cb428a2aa03df09
 compiler/typecheck/TcInteract.lhs | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 832b8ee..5870938 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -2092,18 +2092,31 @@ getCoercibleInst (in negated form).
 
 Note [Order of Coercible Instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 At first glance, the order of the various coercible instances 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.
+But because of role annotations, the order *can* matter:
+
+  newtype T a = MkT [a]
+  type role T nominal
+
+  type family F a
+  type instance F Int = Bool
+
+Here T's declared role is more restrictive than its inferred role
+(representational) would be.  If MkT is not in scope, so that the
+newtype-unwrapping instance is not available, then this coercible
+instance would fail:
+  Coercible (T Bool) (T (F Int)
+But MkT was in scope, *and* if we used it before decomposing on T,
+we'd unwrap the newtype (on both sides) to get
+  Coercible Bool (F Int)
+whic succeeds.
 
+So our current decision is to apply case 3 (newtype-unwrapping) first,
+followed by decomposition (case 4).  This is strictly more powerful 
+if the newtype constructor is in scope.  See Trac #9117 for a discussion.
 
 Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~