[commit: ghc] wip/new-flatten-skolems-Aug14: Another traceTc debug trace (c7b6d41)

[git at git.haskell.org]

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

On branch  : wip/new-flatten-skolems-Aug14
Link       : http://ghc.haskell.org/trac/ghc/changeset/c7b6d418d3a85b0d73b32d2d6eba45b17216b5f3/ghc

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

commit c7b6d418d3a85b0d73b32d2d6eba45b17216b5f3
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Sep 30 21:29:18 2014 +0100

    Another traceTc debug trace


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

c7b6d418d3a85b0d73b32d2d6eba45b17216b5f3
 compiler/typecheck/Flattening-notes | 36 ++++++++++++++++++++++++------------
 compiler/typecheck/Inst.lhs         |  7 ++++++-
 2 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/compiler/typecheck/Flattening-notes b/compiler/typecheck/Flattening-notes
index f31d3b4..a945d03 100644
--- a/compiler/typecheck/Flattening-notes
+++ b/compiler/typecheck/Flattening-notes
@@ -11,6 +11,8 @@ ToDo:
 
 * TcCanonical re-orients, so TcInteract should
   not do so.  (TwoWay, OneWay)
+* Check orientation (isFlattenTyVar) in canEqTyVarTyVar
+
 
 * No need to zonk now we are unflattening
 
@@ -20,22 +22,10 @@ ToDo:
    They are all CFunEqCans, CTyEqCans
 
 * Update Note [Preparing inert set for implications]
-
-* indexed_types/should_compile/T3826
-
-* remove level from FlatSkol -- not needed now they always
-  come from current level
-
-* remove the (b) CFunEqCan in simpl_loop
-
-* remove fe_rewrite_same
-
 * remove/rewrite TcMType Note [Unflattening while zonking]
 
 * Consider individual data tpyes for CFunEqCan etc
 
-* Check orientation (isFlattenTyVar) in canEqTyVarTyVar
-
 ----------------------
 Outer given is rewritten by an inner given, then there must have been an inner given equality, hence the “given-eq” flag will be true anyway.
 
@@ -67,6 +57,28 @@ We want: alpha := beta (which might unlock something else).  So rewriting wanted
 
 
 ----------------------------------------
+indexed-types/should_failt/T4179
+
+after solving
+  [W] fuv_1 ~ fuv_2
+  [W] A3 (FCon x)           ~ fuv_1    (CFunEqCan)
+  [W] A3 (x (aoa -> fuv_2)) ~ fuv_2    (CFunEqCan)
+
+----------------------------------------
+indexed-types/should_fail/T7729a
+
+a)  [W]   BasePrimMonad (Rand m) ~ m1
+b)  [W]   tt m1 ~ BasePrimMonad (Rand m)
+
+--->  process (b) first
+    BasePrimMonad (Ramd m) ~ fuv_atH
+    fuv_atH ~ tt m1
+  
+--->  now process (a)
+    m1 ~ s_atH ~ tt m1    -- An obscure occurs check
+
+
+----------------------------------------
 typecheck/TcTypeNatSimple
 
 Original constraint
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index ed77706..758081e 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -169,7 +169,12 @@ deeplyInstantiate orig ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
   = do { (_, tys, subst) <- tcInstTyVars tvs
        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
-       ; wrap1 <- instCall orig tys (substTheta subst theta)
+       ; let theta' = substTheta subst theta
+       ; wrap1 <- instCall orig tys theta'
+       ; traceTc "Instantiating (deply)" (vcat [ ppr ty
+                                               , text "with" <+> ppr tys
+                                               , text "args:" <+> ppr ids1
+                                               , text "theta:" <+>  ppr theta' ])
        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
        ; return (mkWpLams ids1
                     <.> wrap2