[commit: ghc] wip/impredicativity: Add extra rule to InstanceOf canon + better variable flagging (eb9dff6)

[git at git.haskell.org]

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

On branch  : wip/impredicativity
Link       : http://ghc.haskell.org/trac/ghc/changeset/eb9dff6556b69ac612d203224c89bccd91dbfbba/ghc

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

commit eb9dff6556b69ac612d203224c89bccd91dbfbba
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Thu Jun 25 15:35:03 2015 +0200

    Add extra rule to InstanceOf canon + better variable flagging
    
    - The new rule is InstanceOf (forall a. Q => a) ty
                  --> Q[a -> alpha] /\ alpha ~ ty
                  --> Q[ty]
      This is needed because in many cases when using type classes
      we come to a point where we have
        InstanceOf (forall a. C a => a) b
      and if b is a variable, we cannot continue further without
      this new rule, leaving unsolved constraints.
    
    - The flags for variables (whether on instantiation they will
      receive an instantiation or a equality constraint) have been
      rethought and flipped in some cases.


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

eb9dff6556b69ac612d203224c89bccd91dbfbba
 compiler/typecheck/TcBinds.hs     |  2 +-
 compiler/typecheck/TcCanonical.hs | 25 +++++++++++++++++++++++++
 compiler/typecheck/TcRnDriver.hs  |  2 +-
 compiler/typecheck/TcRules.hs     |  2 +-
 4 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index a818919..c00bd8f 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -387,7 +387,7 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
 
     go :: [SCC (LHsBind Name)] -> TcM (LHsBinds TcId, thing)
     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
-                        ; let uids1 = map (\x -> (x, TcIdMonomorphic)) ids1
+                        ; let uids1 = map (\x -> (x, TcIdUnrestricted)) ids1
                         ; (binds2, thing) <- tcExtendLetEnv top_lvl uids1 $
                                              go sccs
                         ; return (binds1 `unionBags` binds2, thing) }
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index fd7a191..05d564e 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1663,6 +1663,31 @@ can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
     -- case InstanceOf (T ...) sigma --> T ... ~ sigma
   | Nothing <- getTyVar_maybe lhs, Nothing <- splitForAllTy_maybe lhs
   = can_instance_to_eq ev lhs rhs
+  -- case InstanceOf (forall a. Q => a) sigma, sigma without forall.
+  -- in this case, this is equivalent to Q[a -> sigma]
+  | (_:_, _, v) <- tcSplitSigmaTy lhs, Just _ <- getTyVar_maybe v
+  , Nothing <- splitForAllTy_maybe rhs
+  = case ev of
+      CtWanted { ctev_evar = evar, ctev_loc = loc } ->
+        do { (qvars, q, ty) <- splitInst lhs
+             -- generate new constraints
+           ; new_ev_qs <- mapM (newWantedEvVarNC loc) q
+           ; let qvars' = map mkTyVarTy qvars
+             -- generate inner instantiation
+           ; let inst = mkInstanceOfPred ty rhs
+           ; inst_ev <- newWantedEvVarNC loc inst
+           ; let eq = mkEqPred ty rhs
+           ; eq_ev <- newWantedEvVarNC loc eq
+             -- compute the evidence for the instantiation
+           ; setWantedEvBind (ctev_evar inst_ev)
+                             (mkInstanceOfEq ty (ctEvCoercion eq_ev))
+           ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvId inst_ev)
+                                                    (map ctev_evar new_ev_qs))
+             -- emit new work
+           ; emitWorkNC new_ev_qs
+           ; traceTcS "can_instance_of/INST/Top" (vcat [ ppr eq_ev, ppr new_ev_qs ])
+           ; canEqNC eq_ev NomEq ty rhs }
+      _ -> stopWith ev "Given/Derived instanceOf instantiation"
   -- case InstanceOf (forall qvars. Q => ty) (T ...)
   | Nothing <- getTyVar_maybe rhs, Nothing <- splitForAllTy_maybe rhs
   , Just _  <- splitForAllTy_maybe lhs
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 4fa8a4e..39f5814 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1453,7 +1453,7 @@ runTcInteractive hsc_env thing_inside
       , NotTopLevel <- isClosedLetBndr id
       = Left (idName id, ATcId { tct_id = id
                                , tct_closed = NotTopLevel
-                               , tct_flavor = TcIdMonomorphic })
+                               , tct_flavor = TcIdUnrestricted })
       | otherwise
       = Right thing
 
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index b948592..80db8c8 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -68,7 +68,7 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
               -- the RULE.  c.f. Trac #10072
 
        ; let (id_bndrs, tv_bndrs) = partition isId vars
-             id_bndrs' = [(id_bndr, TcIdMonomorphic) | id_bndr <- id_bndrs]
+             id_bndrs' = [(id_bndr, TcIdUnrestricted) | id_bndr <- id_bndrs]
        ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
             <- tcExtendTyVarEnv tv_bndrs  $
                tcExtendIdEnv    id_bndrs' $