A collection of type-inference refactorings.
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 20 Sep 2016 22:31:07 +0000 (23:31 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Oct 2016 16:15:48 +0000 (17:15 +0100)
This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling

79 files changed:
compiler/ghci/RtClosureInspect.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcPluginM.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Type.hs
compiler/vectorise/Vectorise/Generic/PData.hs
testsuite/tests/ado/ado004.stderr
testsuite/tests/annotations/should_fail/annfail10.stderr
testsuite/tests/driver/T2182.stderr
testsuite/tests/gadt/gadt-escape1.stderr
testsuite/tests/gadt/gadt13.stderr
testsuite/tests/gadt/gadt7.stderr
testsuite/tests/ghci.debugger/scripts/break012.stdout
testsuite/tests/ghci.debugger/scripts/print022.stdout
testsuite/tests/ghci/scripts/T11524a.stdout
testsuite/tests/ghci/scripts/T2182ghci.stderr
testsuite/tests/indexed-types/should_fail/T12386.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T12386.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T7354.stderr
testsuite/tests/parser/should_compile/read014.stderr
testsuite/tests/parser/should_fail/T7848.stderr
testsuite/tests/parser/should_fail/readFail003.stderr
testsuite/tests/partial-sigs/should_compile/T10438.stderr
testsuite/tests/partial-sigs/should_compile/T11192.stderr
testsuite/tests/patsyn/should_compile/T11213.stderr
testsuite/tests/patsyn/should_fail/mono.stderr
testsuite/tests/polykinds/T7438.stderr
testsuite/tests/rebindable/rebindable6.stderr
testsuite/tests/rename/should_compile/T12597.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/simplCore/should_compile/noinline01.stderr
testsuite/tests/th/T11452.stderr
testsuite/tests/th/T2222.stderr
testsuite/tests/typecheck/should_compile/ExPatFail.stderr
testsuite/tests/typecheck/should_compile/T12427.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T12427a.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/tc141.stderr
testsuite/tests/typecheck/should_fail/T10495.stderr
testsuite/tests/typecheck/should_fail/T10619.stderr
testsuite/tests/typecheck/should_fail/T12177.stderr
testsuite/tests/typecheck/should_fail/T3102.hs
testsuite/tests/typecheck/should_fail/T3102.stderr
testsuite/tests/typecheck/should_fail/T7453.stderr
testsuite/tests/typecheck/should_fail/T7734.stderr
testsuite/tests/typecheck/should_fail/T9109.stderr
testsuite/tests/typecheck/should_fail/T9318.stderr
testsuite/tests/typecheck/should_fail/VtaFail.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail002.stderr
testsuite/tests/typecheck/should_fail/tcfail004.stderr
testsuite/tests/typecheck/should_fail/tcfail005.stderr
testsuite/tests/typecheck/should_fail/tcfail013.stderr
testsuite/tests/typecheck/should_fail/tcfail014.stderr
testsuite/tests/typecheck/should_fail/tcfail018.stderr
testsuite/tests/typecheck/should_fail/tcfail032.stderr
testsuite/tests/typecheck/should_fail/tcfail099.stderr
testsuite/tests/typecheck/should_fail/tcfail104.stderr
testsuite/tests/typecheck/should_fail/tcfail140.stderr
testsuite/tests/typecheck/should_fail/tcfail181.stderr
testsuite/tests/warnings/should_compile/T12574.stderr

index 9f671f2..eff2660 100644 (file)
@@ -1218,7 +1218,7 @@ zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
   where
     zonk_unbound_meta tv
       = ASSERT( isTcTyVar tv )
-        do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk
+        do { tv' <- skolemiseRuntimeUnk tv
              -- This is where RuntimeUnks are born:
              -- otherwise-unconstrained unification variables are
              -- turned into RuntimeUnks as they leave the
index f2d3ef0..e5b8020 100644 (file)
@@ -225,7 +225,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 -- if    deeplyInstantiate ty = (wrap, rho)
 -- and   e :: ty
 -- then  wrap e :: rho
--- That is, wrap :: ty "->" rho
+-- That is, wrap :: ty ~> rho
 
 deeplyInstantiate orig ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
@@ -381,7 +381,7 @@ tcInstBinderX _ subst (Anon ty)
      -- This is the *only* constraint currently handled in types.
   | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
   = do { let origin = TypeEqOrigin { uo_actual   = k1
-                                   , uo_expected = mkCheckExpType k2
+                                   , uo_expected = k2
                                    , uo_thing    = Nothing }
        ; co <- case role of
                  Nominal          -> unifyKind noThing k1 k2
index 8fba643..09746d3 100644 (file)
@@ -33,7 +33,6 @@ import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
-import Inst( deeplyInstantiate )
 import FamInstEnv( normaliseType )
 import FamInst( tcGetFamInstEnvs )
 import TyCon
@@ -741,7 +740,7 @@ mkExport prag_fn qtvs theta
                                            -- an ambiguouse type and have AllowAmbiguousType
                                            -- e..g infer  x :: forall a. F a -> Int
                   else addErrCtxtM (mk_impedence_match_msg mono_info sel_poly_ty poly_ty) $
-                       tcSubType_NC sig_ctxt sel_poly_ty (mkCheckExpType poly_ty)
+                       tcSubType_NC sig_ctxt sel_poly_ty poly_ty
 
         ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
         ; when warn_missing_sigs $
@@ -1117,58 +1116,6 @@ for a non-overloaded function.
 
 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
 The signatures have been dealt with already.
-
-Note [Pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~
-The rule for typing pattern bindings is this:
-
-    ..sigs..
-    p = e
-
-where 'p' binds v1..vn, and 'e' may mention v1..vn,
-typechecks exactly like
-
-    ..sigs..
-    x = e       -- Inferred type
-    v1 = case x of p -> v1
-    ..
-    vn = case x of p -> vn
-
-Note that
-    (f :: forall a. a -> a) = id
-should not typecheck because
-       case id of { (f :: forall a. a->a) -> f }
-will not typecheck.
-
-Note [Instantiate when inferring a type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  f = (*)
-As there is no incentive to instantiate the RHS, tcMonoBinds will
-produce a type of forall a. Num a => a -> a -> a for `f`. This will then go
-through simplifyInfer and such, remaining unchanged.
-
-There are two problems with this:
- 1) If the definition were `g _ = (*)`, we get a very unusual type of
-    `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is
-    surely confusing for users.
-
- 2) The monomorphism restriction can't work. The MR is dealt with in
-    simplifyInfer, and simplifyInfer has no way of instantiating. This
-    could perhaps be worked around, but it may be hard to know even
-    when instantiation should happen.
-
-There is an easy solution to both problems: instantiate (deeply) when
-inferring a type. So that's what we do. Note that this decision is
-user-facing.
-
-We do this deep instantiation in tcMonoBinds, in the FunBind case
-only, and only when we do not have a type signature.  Conveniently,
-the fun_co_fn field of FunBind gives a place to record the coercion.
-
-We do not need to do this
- * for PatBinds, because we don't have a function type
- * for FunBinds where we have a signature, bucause we aren't doing inference
 -}
 
 data MonoBindInfo = MBI { mbi_poly_name :: Name
@@ -1193,27 +1140,21 @@ tcMonoBinds is_rec sig_fn no_gen
         -- e.g.         f = \(x::forall a. a->a) -> <body>
         --      We want to infer a higher-rank type for f
     setSrcSpan b_loc    $
-    do  { rhs_ty <- newOpenInferExpType
-        ; (co_fn, matches')
-            <- tcExtendIdBndrs [TcIdBndr_ExpType name rhs_ty NotTopLevel] $
+    do  { ((co_fn, matches'), rhs_ty)
+            <- tcInferInst $ \ exp_ty ->
+                  -- tcInferInst: see TcUnify,
+                  -- Note [Deep instantiation of InferResult]
+               tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
                   -- type of the thing whose rhs we are type checking
-               tcMatchesFun (L nm_loc name) matches rhs_ty
-        ; rhs_ty  <- readExpType rhs_ty
-
-        -- Deeply instantiate the inferred type
-        -- See Note [Instantiate when inferring a type]
-        ; let orig = matchesCtOrigin matches
-        ; rhs_ty <- zonkTcType rhs_ty -- NB: zonk to uncover any foralls
-        ; (inst_wrap, rhs_ty) <- addErrCtxtM (instErrCtxt name rhs_ty) $
-                                 deeplyInstantiate orig rhs_ty
+               tcMatchesFun (L nm_loc name) matches exp_ty
 
         ; mono_id <- newLetBndr no_gen name rhs_ty
         ; return (unitBag $ L b_loc $
                      FunBind { fun_id = L nm_loc mono_id,
                                fun_matches = matches', bind_fvs = fvs,
-                               fun_co_fn = inst_wrap <.> co_fn, fun_tick = [] },
+                               fun_co_fn = co_fn, fun_tick = [] },
                   [MBI { mbi_poly_name = name
                        , mbi_sig       = Nothing
                        , mbi_mono_id   = mono_id }]) }
@@ -1297,7 +1238,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
             -- See Note [Existentials in pattern bindings]
         ; ((pat', nosig_mbis), pat_ty)
             <- addErrCtxt (patMonoBindsCtxt pat grhss) $
-               tcInferInst $ \ exp_ty ->
+               tcInferNoInst $ \ exp_ty ->
                tcLetPat inst_sig_fun no_gen pat exp_ty $
                mapM lookup_info nosig_names
 
@@ -1761,16 +1702,3 @@ patMonoBindsCtxt :: (OutputableBndrId id, Outputable body)
 patMonoBindsCtxt pat grhss
   = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)
 
-instErrCtxt :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
-instErrCtxt name ty env
-  = do { let (env', ty') = tidyOpenType env ty
-       ; return (env', hang (text "When instantiating" <+> quotes (ppr name) <>
-                             text ", initially inferred to have" $$
-                             text "this overly-general type:")
-                          2 (ppr ty') $$
-                       extra) }
-  where
-    extra = sdocWithDynFlags $ \dflags ->
-            ppWhen (xopt LangExt.MonomorphismRestriction dflags) $
-            text "NB: This instantiation can be caused by the" <+>
-            text "monomorphism restriction."
index f82fc47..7cf688d 100644 (file)
@@ -142,9 +142,11 @@ reportUnsolved wanted
                                 | warn_out_of_scope      = HoleWarn
                                 | otherwise              = HoleDefer
 
-       ; report_unsolved (Just binds_var) False type_errors expr_holes
+       ; report_unsolved binds_var False type_errors expr_holes
           type_holes out_of_scope_holes wanted
-       ; getTcEvBinds binds_var }
+
+       ; ev_binds <- getTcEvBindsMap binds_var
+       ; return (evBindMapBinds ev_binds)}
 
 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
 -- However, do not make any evidence bindings, because we don't
@@ -155,17 +157,21 @@ reportUnsolved wanted
 -- and for simplifyDefault.
 reportAllUnsolved :: WantedConstraints -> TcM ()
 reportAllUnsolved wanted
-  = report_unsolved Nothing False TypeError HoleError HoleError HoleError wanted
+  = do { ev_binds <- newTcEvBinds
+       ; report_unsolved ev_binds False TypeError
+                         HoleError HoleError HoleError wanted }
 
 -- | Report all unsolved goals as warnings (but without deferring any errors to
 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
 -- TcSimplify
 warnAllUnsolved :: WantedConstraints -> TcM ()
 warnAllUnsolved wanted
-  = report_unsolved Nothing True TypeWarn HoleWarn HoleWarn HoleWarn wanted
+  = do { ev_binds <- newTcEvBinds
+       ; report_unsolved ev_binds True TypeWarn
+                         HoleWarn HoleWarn HoleWarn wanted }
 
 -- | Report unsolved goals as errors or warnings.
-report_unsolved :: Maybe EvBindsVar  -- cec_binds
+report_unsolved :: EvBindsVar        -- cec_binds
                 -> Bool              -- Errors as warnings
                 -> TypeErrorChoice   -- Deferred type errors
                 -> HoleChoice        -- Expression holes
@@ -277,21 +283,15 @@ data ReportErrCtxt
                                        -- ic_skols and givens are tidied, rest are not
           , cec_tidy  :: TidyEnv
 
-          , cec_binds :: Maybe EvBindsVar
-                         -- Nothing <=> Report all errors, including holes
-                         --             Do not add any evidence bindings, because
-                         --             we have no convenient place to put them
-                         --             See TcErrors.reportAllUnsolved
-                         -- Just ev <=> make some errors (depending on cec_defer)
-                         --             into warnings, and emit evidence bindings
-                         --             into 'ev' for unsolved constraints
+          , cec_binds :: EvBindsVar    -- Make some errors (depending on cec_defer)
+                                       -- into warnings, and emit evidence bindings
+                                       -- into 'cec_binds' for unsolved constraints
 
           , cec_errors_as_warns :: Bool   -- Turn all errors into warnings
                                           -- (except for Holes, which are
                                           -- controlled by cec_type_holes and
                                           -- cec_expr_holes)
           , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
-                                                     -- Irrelevant if cec_binds = Nothing
 
           -- cec_expr_holes is a union of:
           --   cec_type_holes - a set of typed holes: '_', '_a', '_foo'
@@ -325,7 +325,7 @@ Specifically (see reportWanteds)
 
 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
-                                 , ic_wanted = wanted, ic_binds = m_evb
+                                 , ic_wanted = wanted, ic_binds = evb
                                  , ic_status = status, ic_info = info
                                  , ic_env = tcl_env, ic_tclvl = tc_lvl })
   | BracketSkol <- info
@@ -356,11 +356,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                       -- tree rooted here, or we've come across
                       -- a suppress-worthy constraint higher up (Trac #11541)
 
-                 , cec_binds    = cec_binds ctxt *> m_evb }
-                      -- If cec_binds ctxt is Nothing, that means
-                      -- we're reporting *all* errors. Don't change
-                      -- that behavior just because we're going into
-                      -- an implication.
+                 , cec_binds    = evb }
 
     dead_givens = case status of
                     IC_Solved { ics_dead = dead } -> dead
@@ -754,12 +750,12 @@ addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
 addDeferredBinding ctxt err ct
   | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
     -- Only add deferred bindings for Wanted constraints
-  , Just ev_binds_var <- cec_binds ctxt  -- We have somewhere to put the bindings
   = do { dflags <- getDynFlags
        ; let err_msg = pprLocErrMsg err
              err_fs  = mkFastString $ showSDoc dflags $
                        err_msg $$ text "(deferred type error)"
              err_tm  = EvDelayedError pred err_fs
+             ev_binds_var = cec_binds ctxt
 
        ; case dest of
            EvVarDest evar
@@ -1537,8 +1533,8 @@ mkEqInfoMsg ct ty1 ty2
     -- mismatched types for suggestion about -fprint-explicit-kinds
     (act_ty, exp_ty) = case ctOrigin ct of
       TypeEqOrigin { uo_actual = act
-                   , uo_expected = Check exp } -> (act, exp)
-      _                                        -> (ty1, ty2)
+                   , uo_expected = exp } -> (act, exp)
+      _                                  -> (ty1, ty2)
 
     invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
               , not vis
@@ -1706,7 +1702,7 @@ mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
 -- NotSwapped means (actual, expected), IsSwapped is the reverse
 -- First return val is whether or not to print a herald above this msg
 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
-                                          , uo_expected = Check exp
+                                          , uo_expected = exp
                                           , uo_thing = maybe_thing })
                     m_level printExpanded
   | KindLevel <- level, occurs_check_error       = (True, Nothing, empty)
index aaa1f0c..ae98d38 100644 (file)
@@ -13,7 +13,7 @@ module TcEvidence (
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
   EvBindMap(..), emptyEvBindMap, extendEvBinds,
-  lookupEvBind, evBindMapBinds, foldEvBindMap,
+  lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
   sccEvBinds, evBindVar,
   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
@@ -283,8 +283,24 @@ data TcEvBinds
   | EvBinds             -- Immutable after zonking
        (Bag EvBind)
 
-data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
-     -- The Unique is for debug printing only
+data EvBindsVar
+  = EvBindsVar {
+      ebv_uniq :: Unique,
+         -- The Unique is for debug printing only
+
+      ebv_binds :: IORef EvBindMap,
+      -- The main payload: the value-level evidence bindings
+      --     (dictionaries etc)
+
+      ebv_tcvs :: IORef TyCoVarSet
+      -- The free vars of the (rhss of) the coercion bindings
+      --
+      -- Coercions don't actually have bindings
+      -- because we plug them in-place (via a mutable
+      -- variable); but we keep their free variables
+      -- so that we can report unused given constraints
+      -- See Note [Tracking redundant constraints] in TcSimplify
+    }
 
 instance Data.Data TcEvBinds where
   -- Placeholder; we can't travers into TcEvBinds
@@ -325,6 +341,9 @@ extendEvBinds bs ev_bind
                                                (eb_lhs ev_bind)
                                                ev_bind }
 
+isEmptyEvBindMap :: EvBindMap -> Bool
+isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
+
 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
 
@@ -334,6 +353,9 @@ evBindMapBinds = foldEvBindMap consBag emptyBag
 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
 
+instance Outputable EvBindMap where
+  ppr (EvBindMap m) = ppr m
+
 -----------------
 -- All evidence is bound by EvBinds; no side effects
 data EvBind
@@ -761,10 +783,11 @@ instance Outputable TcEvBinds where
   ppr (EvBinds bs)  = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
 
 instance Outputable EvBindsVar where
-  ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u)
+  ppr (EvBindsVar { ebv_uniq = u })
+     = text "EvBindsVar" <> angleBrackets (ppr u)
 
 instance Uniquable EvBindsVar where
-  getUnique (EvBindsVar _ u) = u
+  getUnique (EvBindsVar { ebv_uniq = u }) = u
 
 instance Outputable EvBind where
   ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
index 8ae454c..c960f6c 100644 (file)
@@ -141,7 +141,7 @@ tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr)
 
 tcInferSigmaNC (L loc expr)
   = setSrcSpan loc $
-    do { (expr', sigma) <- tcInfer (tcExpr expr)
+    do { (expr', sigma) <- tcInferNoInst (tcExpr expr)
        ; return (L loc expr', sigma) }
 
 tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
@@ -1176,14 +1176,10 @@ tcInferFun (L loc (HsRecFld f))
        ; return (L loc fun, ty) }
 
 tcInferFun fun
-  = do { (fun, fun_ty) <- tcInferSigma fun
+  = tcInferSigma fun
+      -- NB: tcInferSigma; see TcUnify
+      -- Note [Deep instantiation of InferResult]
 
-         -- Zonk the function type carefully, to expose any polymorphism
-         -- E.g. (( \(x::forall a. a->a). blah ) e)
-         -- We can see the rank-2 type of the lambda in time to generalise e
-       ; fun_ty' <- zonkTcType fun_ty
-
-       ; return (fun, fun_ty') }
 
 ----------------
 -- | Type-check the arguments to a function, possibly including visible type
@@ -1267,7 +1263,7 @@ tcTupArgs args tys
 tcSyntaxOp :: CtOrigin
            -> SyntaxExpr Name
            -> [SyntaxOpType]           -- ^ shape of syntax operator arguments
-           -> ExpType                  -- ^ overall result type
+           -> ExpRhoType               -- ^ overall result type
            -> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments
            -> TcM (a, SyntaxExpr TcId)
 -- ^ Typecheck a syntax operator
@@ -1365,7 +1361,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
         herald = text "This rebindable syntax expects a function with"
 
     go rho_ty (SynType the_ty)
-      = do { wrap   <- tcSubTypeET orig the_ty rho_ty
+      = do { wrap   <- tcSubTypeET orig GenSigCtxt the_ty rho_ty
            ; result <- thing_inside []
            ; return (result, wrap) }
 
@@ -1507,8 +1503,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                  then return idHsWrapper  -- Fast path; also avoids complaint when we infer
                                           -- an ambiguouse type and have AllowAmbiguousType
                                           -- e..g infer  x :: forall a. F a -> Int
-                 else tcSubType_NC ExprSigCtxt inferred_sigma
-                                   (mkCheckExpType my_sigma)
+                 else tcSubType_NC ExprSigCtxt inferred_sigma my_sigma
 
        ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
        ; let poly_wrap = wrap
@@ -1581,6 +1576,7 @@ tcInferRecSelId (Ambiguous lbl _)
 ------------------------
 tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType)
 -- Look up an occurrence of an Id
+-- Do not instantiate its type
 tcInferId id_name
   | id_name `hasKey` tagToEnumKey
   = failWithTc (text "tagToEnum# must appear applied to one argument")
@@ -1750,7 +1746,7 @@ tcSeq loc fun_name args res_ty
               -> do { rr_ty <- newFlexiTyVarTy runtimeRepTy
                     ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty)
                                    -- see Note [Typing rule for seq]
-                    ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg2 res_ty
+                    ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg2 res_ty
                     ; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) }
             [Left term_arg1, Left term_arg2]
               -> return (term_arg1, term_arg2, res_ty)
@@ -1773,7 +1769,7 @@ tcTagToEnum loc fun_name args res_ty
        ; arg <- case args of
            [Right hs_ty_arg, Left term_arg]
              -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind
-                   ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg res_ty
+                   ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg res_ty
                      -- other than influencing res_ty, we just
                      -- don't care about a type arg passed in.
                      -- So drop the evidence.
index efb7dfe..618c3c0 100644 (file)
@@ -1445,8 +1445,9 @@ zonk_tc_ev_binds env (TcEvBinds var) = zonkEvBindsVar env var
 zonk_tc_ev_binds env (EvBinds bs)    = zonkEvBinds env bs
 
 zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
-zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
-                                           ; zonkEvBinds env (evBindMapBinds bs) }
+zonkEvBindsVar env (EvBindsVar { ebv_binds = ref })
+  = do { bs <- readMutVar ref
+       ; zonkEvBinds env (evBindMapBinds bs) }
 
 zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
 zonkEvBinds env binds
@@ -1598,7 +1599,7 @@ zonkTvSkolemising :: UnboundTyVarZonker
 -- This variant is used for the LHS of rules
 -- See Note [Zonking the LHS of a RULE].
 zonkTvSkolemising tv
-  = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+  = do { tv' <- skolemiseUnboundMetaTyVar tv
        ; return (mkTyVarTy tv') }
 
 zonkTypeZapping :: UnboundTyVarZonker
index 055159d..2d3dee9 100644 (file)
@@ -853,7 +853,7 @@ checkExpectedKind :: TcType               -- the type whose kind we're checking
 checkExpectedKind ty act_kind exp_kind
  = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
-                                  , uo_expected = mkCheckExpType exp_kind
+                                  , uo_expected = exp_kind
                                   , uo_thing    = Just $ mkTypeErrorThing ty'
                                   }
       ; co_k <- uType origin KindLevel act_kind' exp_kind
@@ -1276,7 +1276,8 @@ kcHsTyVarBndrs name cusk open_fam all_kind_vars
           , hsq_dependent = dep_names }) thing_inside
   | cusk
   = do { kv_kinds <- mk_kv_kinds
-       ; let scoped_kvs = zipWith mk_skolem_tv kv_ns kv_kinds
+       ; lvl <- getTcLevel
+       ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
        ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
     do { (tc_binders, res_kind, stuff) <- solveEqualities $
                                           bind_telescope hs_tvs thing_inside
@@ -1527,14 +1528,16 @@ tcHsTyVarName m_kind name
            _ -> do { kind <- case m_kind of
                                Just kind -> return kind
                                Nothing   -> newMetaKindVar
-                   ; return (mk_skolem_tv name kind, False) }}
+                   ; tv <- newSkolemTyVar name kind
+                   ; return (tv, False) }}
 
 -- makes a new skolem tv
 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
-newSkolemTyVar name kind = return (mk_skolem_tv name kind)
+newSkolemTyVar name kind = do { lvl <- getTcLevel
+                              ; return (mk_skolem_tv lvl name kind) }
 
-mk_skolem_tv :: Name -> Kind -> TcTyVar
-mk_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv
+mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar
+mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False)
 
 ------------------
 kindGeneralizeType :: Type -> TcM Type
@@ -1810,7 +1813,7 @@ tcHsPartialSigType ctxt sig_ty
         ; tau     <- zonkTcType tau
         ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
 
-        ; traceTc "tcHsPatSigType" (ppr all_tvs)
+        ; traceTc "tcHsPartialSigType" (ppr all_tvs)
         ; return (wcs, wcx, all_tvs, theta, tau) }
   where
     new_implicit_tv name = do { kind <- newMetaKindVar
@@ -1889,7 +1892,7 @@ tcPatSig in_pat_bind sig res_ty
         ; if null sig_tvs then do {
                 -- Just do the subsumption check and return
                   wrap <- addErrCtxtM (mk_msg sig_ty) $
-                          tcSubTypeET_NC PatSigCtxt res_ty sig_ty
+                          tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
                 ; return (sig_ty, [], sig_wcs, wrap)
         } else do
                 -- Type signature binds at least one scoped type variable
@@ -1912,7 +1915,7 @@ tcPatSig in_pat_bind sig res_ty
 
         -- Now do a subsumption check of the pattern signature against res_ty
         ; wrap <- addErrCtxtM (mk_msg sig_ty) $
-                  tcSubTypeET_NC PatSigCtxt res_ty sig_ty
+                  tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
 
         -- Phew!
         ; return (sig_ty, sig_tvs, sig_wcs, wrap)
index ab5b75c..aa97075 100644 (file)
@@ -810,7 +810,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                                   , ic_given  = dfun_ev_vars
                                   , ic_wanted = mkImplicWC sc_meth_implics
                                   , ic_status = IC_Unsolved
-                                  , ic_binds  = Just dfun_ev_binds_var
+                                  , ic_binds  = dfun_ev_binds_var
                                   , ic_env    = env
                                   , ic_info   = InstSkol }
 
@@ -1017,7 +1017,7 @@ checkInstConstraints thing_inside
                              , ic_given  = []
                              , ic_wanted = wanted
                              , ic_status = IC_Unsolved
-                             , ic_binds  = Just ev_binds_var
+                             , ic_binds  = ev_binds_var
                              , ic_env    = env
                              , ic_info   = InstSkol }
 
@@ -1368,8 +1368,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
                    ; sig_ty  <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty
                    ; let local_meth_ty = idType local_meth_id
                    ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
-                                tcSubType ctxt (Just sel_id) sig_ty
-                                          (mkCheckExpType local_meth_ty)
+                                tcSubType_NC ctxt sig_ty local_meth_ty
                    ; return (sig_ty, hs_wrap) }
 
        ; inner_meth_name <- newName (nameOccName sel_name)
index 678661c..0f8bf06 100644 (file)
@@ -30,9 +30,11 @@ module TcMType (
   --------------------------------
   -- Expected types
   ExpType(..), ExpSigmaType, ExpRhoType,
-  mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe,
-  writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType,
-  tauifyExpType,
+  mkCheckExpType,
+  newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
+  readExpType, readExpType_maybe,
+  expTypeToType, checkingExpType_maybe, checkingExpType,
+  tauifyExpType, inferResultToType, promoteTcType,
 
   --------------------------------
   -- Creating fresh type variables for pm checking
@@ -66,7 +68,7 @@ module TcMType (
   zonkTidyTcType, zonkTidyOrigin,
   mkTypeErrorThing, mkTypeErrorThingArgs,
   tidyEvVar, tidyCt, tidySkolemInfo,
-  skolemiseUnboundMetaTyVar,
+  skolemiseUnboundMetaTyVar, skolemiseRuntimeUnk,
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
   zonkTyCoVarsAndFV, zonkTcTypeAndFV,
   zonkTyCoVarsAndFVList,
@@ -335,21 +337,29 @@ test gadt/gadt-escape1.
 -- actual data definition is in TcType
 
 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
-newOpenInferExpType :: TcM ExpType
-newOpenInferExpType
+newInferExpTypeNoInst :: TcM ExpSigmaType
+newInferExpTypeNoInst = newInferExpType False
+
+newInferExpTypeInst :: TcM ExpRhoType
+newInferExpTypeInst = newInferExpType True
+
+newInferExpType :: Bool -> TcM ExpType
+newInferExpType inst
   = do { rr <- newFlexiTyVarTy runtimeRepTy
        ; u <- newUnique
        ; tclvl <- getTcLevel
        ; let ki = tYPE rr
        ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
        ; ref <- newMutVar Nothing
-       ; return (Infer u tclvl ki ref) }
+       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
+                           , ir_kind = ki, ir_ref = ref
+                           , ir_inst = inst })) }
 
 -- | Extract a type out of an ExpType, if one exists. But one should always
 -- exist. Unless you're quite sure you know what you're doing.
 readExpType_maybe :: ExpType -> TcM (Maybe TcType)
-readExpType_maybe (Check ty)        = return (Just ty)
-readExpType_maybe (Infer _ _ _ ref) = readMutVar ref
+readExpType_maybe (Check ty)                   = return (Just ty)
+readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
 
 -- | Extract a type out of an ExpType. Otherwise, panics.
 readExpType :: ExpType -> TcM TcType
@@ -359,30 +369,6 @@ readExpType exp_ty
            Just ty -> return ty
            Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
 
--- | Write into an 'ExpType'. It must be an 'Infer'.
-writeExpType :: ExpType -> TcType -> TcM ()
-writeExpType (Infer u tc_lvl ki ref) ty
-  | debugIsOn
-  = do { ki1 <- zonkTcType (typeKind ty)
-       ; ki2 <- zonkTcType ki
-       ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
-       ; lvl_now <- getTcLevel
-       ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now )
-       ; cts <- readTcRef ref
-       ; case cts of
-           Just already_there -> pprPanic "writeExpType"
-                                   (vcat [ ppr u
-                                         , ppr ty
-                                         , ppr already_there ])
-           Nothing -> write }
-  | otherwise
-  = write
-  where
-    write = do { traceTc "Filling ExpType" $
-                   ppr u <+> text ":=" <+> ppr ty
-               ; writeTcRef ref (Just ty) }
-writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2)
-
 -- | Returns the expected type when in checking mode.
 checkingExpType_maybe :: ExpType -> Maybe TcType
 checkingExpType_maybe (Check ty) = Just ty
@@ -397,35 +383,132 @@ checkingExpType err et         = pprPanic "checkingExpType" (text err $$ ppr et)
 tauifyExpType :: ExpType -> TcM ExpType
 -- ^ Turn a (Infer hole) type into a (Check alpha),
 -- where alpha is a fresh unificaiton variable
-tauifyExpType (Check ty)              = return (Check ty)  -- No-op for (Check ty)
-tauifyExpType (Infer u tc_lvl ki ref) = do { ty <- inferTypeToType u tc_lvl ki ref
-                                           ; return (Check ty) }
+tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
+tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
+                                   ; return (Check ty) }
 
 -- | Extracts the expected type if there is one, or generates a new
 -- TauTv if there isn't.
 expTypeToType :: ExpType -> TcM TcType
-expTypeToType (Check ty)              = return ty
-expTypeToType (Infer u tc_lvl ki ref) = inferTypeToType u tc_lvl ki ref
-
-inferTypeToType :: Unique -> TcLevel -> Kind -> IORef (Maybe TcType) -> TcM Type
-inferTypeToType u tc_lvl ki ref
-  = do { uniq <- newUnique
-       ; tv_ref <- newMutVar Flexi
-       ; let details = MetaTv { mtv_info = TauTv
-                              , mtv_ref  = tv_ref
-                              , mtv_tclvl = tc_lvl }
-             name   = mkMetaTyVarName uniq (fsLit "t")
-             tau_tv = mkTcTyVar name ki details
-             tau    = mkTyVarTy tau_tv
-             -- can't use newFlexiTyVarTy because we need to set the tc_lvl
-             -- See also Note [TcLevel of ExpType]
-
+expTypeToType (Check ty)      = return ty
+expTypeToType (Infer inf_res) = inferResultToType inf_res
+
+inferResultToType :: InferResult -> TcM Type
+inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
+                      , ir_kind = kind, ir_ref = ref })
+  = do { tau_tv <- newMetaTyVarAtLevel tc_lvl kind
+             -- See Note [TcLevel of ExpType]
+       ; let tau = mkTyVarTy tau_tv
        ; writeMutVar ref (Just tau)
        ; traceTc "Forcing ExpType to be monomorphic:"
-                 (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau)
+                 (ppr u <+> dcolon <+> ppr kind <+> text ":=" <+> ppr tau)
        ; return tau }
 
-{-
+{- *********************************************************************
+*                                                                      *
+              Promoting types
+*                                                                      *
+********************************************************************* -}
+
+promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
+-- See Note [Promoting a type]
+-- promoteTcType level ty = (co, ty')
+--   * Returns ty' whose max level is just 'level'
+--             and whose kind is the same as 'ty'
+--   * and co :: ty ~ ty'
+--   * and emits constraints to justify the coercion
+promoteTcType dest_lvl ty
+  = do { cur_lvl <- getTcLevel
+       ; if (cur_lvl `sameDepthAs` dest_lvl)
+         then dont_promote_it
+         else promote_it }
+  where
+    promote_it :: TcM (TcCoercion, TcType)
+    promote_it
+      = do { prom_tv <- newMetaTyVarAtLevel dest_lvl (typeKind ty)
+           ; let prom_ty = mkTyVarTy prom_tv
+                 eq_orig = TypeEqOrigin { uo_actual   = ty
+                                        , uo_expected = prom_ty
+                                        , uo_thing    = Nothing }
+
+           ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
+           ; return (co, prom_ty) }
+
+    dont_promote_it :: TcM (TcCoercion, TcType)
+    dont_promote_it = return (mkTcNomReflCo ty, ty)
+
+{- Note [Promoting a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #12427)
+
+  data T where
+    MkT :: (Int -> Int) -> a -> T
+
+  h y = case y of MkT v w -> v
+
+We'll infer the RHS type with an expected type ExpType of
+  (IR { ir_lvl = l, ir_ref = ref, ... )
+where 'l' is the TcLevel of the RHS of 'h'.  Then the MkT pattern
+match will increase the level, so we'll end up in tcSubType, trying to
+unify the type of v,
+  v :: Int -> Int
+with the expected type.  But this attempt takes place at level (l+1),
+rightly so, since v's type could have mentioned existential variables,
+(like w's does) and we want to catch that.
+
+So we
+  - create a new meta-var alpha[l+1]
+  - fill in the InferRes ref cell 'ref' with alpha
+  - emit an equality constraint, thus
+        [W] alpha[l+1] ~ (Int -> Int)
+
+That constraint will float outwards, as it should, unless v's
+type mentions a skolem-captured variable.
+
+This approach fails if v has a higher rank type; see
+Note [Promotion and higher rank types]
+
+
+Note [Promotion and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
+then we'd emit an equality
+        [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
+which will sadly fail because we can't unify a unification variable
+with a polytype.  But there is nothing really wrong with the program
+here.
+
+We could just about solve this by "promote the type" of v, to expose
+its polymorphic "shape" while still leaving constraints that will
+prevent existential escape.  But we must be careful!  Exposing
+the "shape" of the type is precisely what we must NOT do under
+a GADT pattern match!  So in this case we might promote the type
+to
+        (forall a. a->a) -> alpha[l+1]
+and emit the constraint
+        [W] alpha[l+1] ~ Int
+Now the poromoted type can fill the ref cell, while the emitted
+equality can float or not, according to the usual rules.
+
+But that's not quite right!  We are exposing the arrow! We could
+deal with that too:
+        (forall a. mu[l+1] a a) -> alpha[l+1]
+with constraints
+        [W] alpha[l+1] ~ Int
+        [W] mu[l+1] ~ (->)
+Here we abstract over the '->' inside the forall, in case that
+is subject to an equality constraint from a GADT match.
+
+Note that we kept the outer (->) becuase that's part of
+the polymorphic "shape".  And becauuse of impredicativity,
+GADT matches can't give equalities that affect polymorphic
+shape.
+
+This reasoning just seems too complicated, so I decided not
+to do it.  These higher-rank notes are just here to record
+the thinking.
+
+
 ************************************************************************
 *                                                                      *
         SkolemTvs (immutable)
@@ -493,17 +576,22 @@ tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Get the location from the monad; this is a complete freshening operation
 tcInstSkolTyVars' overlappable subst tvs
   = do { loc <- getSrcSpanM
-       ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
+       ; lvl <- getTcLevel
+       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
 
-mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
-mkTcSkolTyVar loc overlappable uniq old_name kind
-  = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
-              kind
-              (SkolemTv overlappable)
+mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker
+mkTcSkolTyVar lvl loc overlappable
+  = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
+                                      kind details
+  where
+    details = SkolemTv (pushTcLevel lvl) overlappable
+              -- NB: skolems bump the level
 
 tcInstSigTyVars :: SrcSpan -> [TyVar]
-                -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
-tcInstSigTyVars loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
+                -> TcM (TCvSubst, [TcTyVar])
+tcInstSigTyVars loc tvs
+  = do { lvl <- getTcLevel
+       ; instSkolTyCoVars (mkTcSkolTyVar lvl loc False) tvs }
 
 ------------------
 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
@@ -522,15 +610,15 @@ freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
     mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
 
 ------------------
-instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
-                 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
+instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
 
-instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
+instSkolTyCoVarsX :: TcTyVarMaker
                   -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
 
-instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
+instSkolTyCoVarX :: TcTyVarMaker
                  -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
 instSkolTyCoVarX mk_tcv subst tycovar
   = do  { uniq <- newUnique  -- using a new unique is critical. See
@@ -620,7 +708,7 @@ cloneMetaTyVar tv
 -- Works for both type and kind variables
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
-                      readMutVar (metaTvRef tyvar)
+                      readMutVar (metaTyVarRef tyvar)
 
 isFilledMetaTyVar :: TyVar -> TcM Bool
 -- True of a filled-in (Indirect) meta type variable
@@ -645,7 +733,7 @@ writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 
 writeMetaTyVar tyvar ty
   | not debugIsOn
-  = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
+  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
 
 -- Everything from here on only happens if DEBUG is on
   | not (isTcTyVar tyvar)
@@ -669,32 +757,61 @@ writeMetaTyVarRef tyvar ref ty
                                    <+> text ":=" <+> ppr ty)
        ; writeTcRef ref (Indirect ty) }
 
--- Everything from here on only happens if DEBUG is on
+  -- Everything from here on only happens if DEBUG is on
   | otherwise
   = do { meta_details <- readMutVar ref;
        -- Zonk kinds to allow the error check to work
        ; zonked_tv_kind <- zonkTcType tv_kind
        ; zonked_ty_kind <- zonkTcType ty_kind
+       ; let kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
+                                               -- to coercion variables
+                          || tcEqKind zonked_ty_kind zonked_tv_kind
+
+             kind_msg = hang (text "Ill-kinded update to meta tyvar")
+                           2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
+                              <+> text ":="
+                              <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )
+
+       ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 
        -- Check for double updates
-       ; ASSERT2( isFlexi meta_details,
-                  hang (text "Double update of meta tyvar")
-                   2 (ppr tyvar $$ ppr meta_details) )
-
-         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
-       ; writeMutVar ref (Indirect ty)
-       ; when (   not (isPredTy tv_kind)
-                    -- Don't check kinds for updates to coercion variables
-               && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
-       $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
-                        2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
-                           <+> text ":="
-                           <+> ppr ty    <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
-         (return ()) }
+       ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
+
+       -- Check for level OK
+       -- See Note [Level check when unifying]
+       ; MASSERT2( level_check_ok, level_check_msg )
+
+       -- Check Kinds ok
+       ; MASSERT2( kind_check_ok, kind_msg )
+
+       -- Do the write
+       ; writeMutVar ref (Indirect ty) }
   where
     tv_kind = tyVarKind tyvar
     ty_kind = typeKind ty
 
+    tv_lvl = tcTyVarLevel tyvar
+    ty_lvl = tcTypeLevel ty
+
+    level_check_ok = isFmvTyVar tyvar
+                  || not (ty_lvl `strictlyDeeperThan` tv_lvl)
+    level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
+
+    double_upd_msg details = hang (text "Double update of meta tyvar")
+                                2 (ppr tyvar $$ ppr details)
+
+
+{- Note [Level check when unifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When unifying
+     alpha:lvl := ty
+we expect that the TcLevel of 'ty' will be <= lvl.
+However, during unflatting we do
+     fuv:l := ty:(l+1)
+which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
+See Note [TcLevel assignment] in TcType.
+-}
+
 {-
 % Generating fresh variables for pattern match check
 -}
@@ -705,7 +822,8 @@ genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
 -- Precondition: tyvars should be scoping-ordered
 -- see Note [Kind substitution when instantiating]
 -- Get the location from the monad; this is a complete freshening operation
-genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
+genInstSkolTyVarsX loc subst tvs
+  = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
 
 {-
 ************************************************************************
@@ -785,16 +903,26 @@ newWildCardX subst tv
        ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
 
 new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-new_meta_tv_x info subst tyvar
+new_meta_tv_x info subst tv
   = do  { uniq <- newUnique
         ; details <- newMetaDetails info
-        ; let name   = mkSystemName uniq (getOccName tyvar)
+        ; let name   = mkSystemName uniq (getOccName tv)
                        -- See Note [Name of an instantiated type variable]
-              kind   = substTy subst (tyVarKind tyvar)
+              kind   = substTy subst (tyVarKind tv)
               new_tv = mkTcTyVar name kind details
-              subst1 = extendTvSubstWithClone subst tyvar new_tv
+              subst1 = extendTvSubstWithClone subst tv new_tv
         ; return (subst1, new_tv) }
 
+newMetaTyVarAtLevel :: TcLevel -> TcKind -> TcM TcTyVar
+newMetaTyVarAtLevel tc_lvl kind
+  = do  { uniq <- newUnique
+        ; ref  <- newMutVar Flexi
+        ; let name = mkMetaTyVarName uniq (fsLit "p")
+              details = MetaTv { mtv_info  = TauTv
+                               , mtv_ref   = ref
+                               , mtv_tclvl = tc_lvl }
+        ; return (mkTcTyVar name kind details) }
+
 {- Note [Name of an instantiated type variable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 At the moment we give a unification variable a System Name, which
@@ -960,7 +1088,7 @@ zonkQuantifiedTyVar default_kind tv
            ; return Nothing }
 
       | otherwise
-      = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+      = do { tv' <- skolemiseUnboundMetaTyVar tv
            ; return (Just tv') }
 
     default_kind_var :: TyVar -> TcM Type
@@ -988,13 +1116,21 @@ zonkQuantifiedTyVar default_kind tv
                Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                               return () }
 
-skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
+skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
+skolemiseRuntimeUnk tv
+  = skolemise_tv tv RuntimeUnk
+
+skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
+skolemiseUnboundMetaTyVar tv
+  = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
+
+skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, so that
 --   we are totally out of Meta-tyvar-land
 -- We create a skolem TyVar, not a regular TyVar
 --   See Note [Zonking to Skolem]
-skolemiseUnboundMetaTyVar tv details
+skolemise_tv tv details
   = ASSERT2( isMetaTyVar tv, ppr tv )
     do  { span <- getSrcSpanM    -- Get the location from "here"
                                  -- ie where we are generalising
@@ -1448,11 +1584,7 @@ zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
                                       , uo_expected = exp
                                       , uo_thing    = m_thing })
   = do { (env1, act') <- zonkTidyTcType env  act
-       ; mb_exp <- readExpType_maybe exp  -- it really should be filled in.
-                                          -- unless we're debugging.
-       ; (env2, exp') <- case mb_exp of
-           Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
-           Nothing -> return (env1, exp)
+       ; (env2, exp') <- zonkTidyTcType env1 exp
        ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
        ; return ( env3, orig { uo_actual   = act'
                              , uo_expected = exp'
index 85a7e30..01586c0 100644 (file)
@@ -869,10 +869,9 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
               tup_ty  = mkBigCoreTupTy tup_elt_tys
 
         ; tcExtendIdEnv tup_ids $ do
-        { stmts_ty <- newOpenInferExpType
-        ; (stmts', (ret_op', tup_rets))
-                <- tcStmtsAndThen ctxt tcDoStmt stmts stmts_ty   $
-                   \ inner_res_ty ->
+        { ((stmts', (ret_op', tup_rets)), stmts_ty)
+                <- tcInferInst $ \ exp_ty ->
+                   tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty ->
                    do { tup_rets <- zipWithM tcCheckId tup_names
                                       (map mkCheckExpType tup_elt_tys)
                              -- Unify the types of the "final" Ids (which may
@@ -881,14 +880,12 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
                           <- tcSyntaxOp DoOrigin ret_op [synKnownType tup_ty]
                                         inner_res_ty $ \_ -> return ()
                       ; return (ret_op', tup_rets) }
-        ; stmts_ty <- readExpType stmts_ty
 
-        ; mfix_res_ty <- newOpenInferExpType
-        ; (_, mfix_op')
-            <- tcSyntaxOp DoOrigin mfix_op
-                          [synKnownType (mkFunTy tup_ty stmts_ty)] mfix_res_ty $
+        ; ((_, mfix_op'), mfix_res_ty)
+            <- tcInferInst $ \ exp_ty ->
+               tcSyntaxOp DoOrigin mfix_op
+                          [synKnownType (mkFunTy tup_ty stmts_ty)] exp_ty $
                \ _ -> return ()
-        ; mfix_res_ty <- readExpType mfix_res_ty
 
         ; ((thing, new_res_ty), bind_op')
             <- tcSyntaxOp DoOrigin bind_op
@@ -1014,7 +1011,7 @@ tcApplicativeStmts
 tcApplicativeStmts ctxt pairs rhs_ty thing_inside
  = do { body_ty <- newFlexiTyVarTy liftedTypeKind
       ; let arity = length pairs
-      ; ts <- replicateM (arity-1) $ newOpenInferExpType
+      ; ts <- replicateM (arity-1) $ newInferExpTypeInst
       ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
       ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
       ; let fun_ty = mkFunTys pat_tys body_ty
index ea4cf3e..9a5fd7d 100644 (file)
@@ -397,7 +397,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
             -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
 
          -- check that overall pattern is more polymorphic than arg type
-        ; expr_wrap2 <- tcSubTypeET (pe_orig penv) overall_pat_ty inf_arg_ty
+        ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
             -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
 
          -- pattern must have inf_res_ty
@@ -502,13 +502,12 @@ tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
 
 ------------------------
 -- Literal patterns
-tc_pat _ (LitPat simple_lit) pat_ty thing_inside
+tc_pat penv (LitPat simple_lit) pat_ty thing_inside
   = do  { let lit_ty = hsLitType simple_lit
-        ; co <- unifyPatType simple_lit lit_ty pat_ty
-                -- coi is of kind: pat_ty ~ lit_ty
-        ; res <- thing_inside
+        ; wrap   <- tcSubTypePat penv pat_ty lit_ty
+        ; res    <- thing_inside
         ; pat_ty <- readExpType pat_ty
-        ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty
+        ; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty
                  , res) }
 
 ------------------------
@@ -622,15 +621,6 @@ tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat)))
 
 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
 
-----------------
-unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
--- In patterns we want a coercion from the
--- context type (expected) to the actual pattern type
--- But we don't want to reverse the args to unifyType because
--- that controls the actual/expected stuff in error messages
-unifyPatType thing actual_ty expected_ty
-  = do { coi <- unifyExpType (Just thing) actual_ty expected_ty
-       ; return (mkTcSymCo coi) }
 
 {-
 Note [Hopping the LIE in lazy patterns]
@@ -841,7 +831,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
               prov_theta' = substTheta tenv prov_theta
               req_theta'  = substTheta tenv req_theta
 
-        ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
+        ; wrap <- tcSubTypePat penv pat_ty ty'
         ; traceTc "tcPatSynPat" (ppr pat_syn $$
                                  ppr pat_ty $$
                                  ppr ty' $$
index dc973da..05d98ff 100644 (file)
@@ -72,11 +72,9 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
        ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
        ; (tclvl, wanted, ((lpat', args), pat_ty))
             <- pushLevelAndCaptureConstraints  $
-               do { pat_ty <- newOpenInferExpType
-                  ; stuff <- tcPat PatSyn lpat pat_ty $
-                             mapM tcLookupId arg_names
-                  ; pat_ty <- readExpType pat_ty
-                  ; return (stuff, pat_ty) }
+               tcInferInst $ \ exp_ty ->
+               tcPat PatSyn lpat exp_ty $
+               mapM tcLookupId arg_names
 
        ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
@@ -390,11 +388,11 @@ tcPatSynMatcher (L loc name) lpat
                 (args, arg_tys) pat_ty
   = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
        ; tv_name <- newNameAt (mkTyVarOcc "r")   loc
-       ; let rr_tv    = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
-             rr       = mkTyVarTy rr_tv
-             res_tv   = mkTcTyVar tv_name  (tYPE rr) (SkolemTv False)
-             is_unlifted = null args && null prov_dicts
+       ; let rr_tv  = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
+             rr     = mkTyVarTy rr_tv
+             res_tv = mkTcTyVar tv_name  (tYPE rr) vanillaSkolemTv
              res_ty = mkTyVarTy res_tv
+             is_unlifted = null args && null prov_dicts
              (cont_args, cont_arg_tys)
                | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
                | otherwise   = (args,                 arg_tys)
index c405440..0363aa1 100644 (file)
@@ -48,8 +48,7 @@ module TcPluginM (
         -- * Manipulating evidence bindings
         newEvVar,
         setEvBind,
-        getEvBindsTcPluginM,
-        getEvBindsTcPluginM_maybe
+        getEvBindsTcPluginM
 #endif
     ) where
 
@@ -64,12 +63,12 @@ import qualified Finder
 
 import FamInstEnv ( FamInstEnv )
 import TcRnMonad  ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM
-                  , unsafeTcPluginTcM, getEvBindsTcPluginM_maybe
+                  , unsafeTcPluginTcM, getEvBindsTcPluginM
                   , liftIO, traceTc )
 import TcMType    ( TcTyVar, TcType )
 import TcEnv      ( TcTyThing )
 import TcEvidence ( TcCoercion, CoercionHole
-                  , EvTerm, EvBind, EvBindsVar, mkGivenEvBind )
+                  , EvTerm, EvBind, mkGivenEvBind )
 import TcRnTypes  ( CtEvidence(..) )
 import Var        ( EvVar )
 
@@ -84,7 +83,6 @@ import Type
 import Id
 import InstEnv
 import FastString
-import Maybes
 import Unique
 
 
@@ -190,12 +188,4 @@ setEvBind :: EvBind -> TcPluginM ()
 setEvBind ev_bind = do
     tc_evbinds <- getEvBindsTcPluginM
     unsafeTcPluginTcM $ TcM.addTcEvBind tc_evbinds ev_bind
-
--- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
--- constraint solving.  This must not be invoked from 'tcPluginInit'
--- or 'tcPluginStop', or it will panic.
-getEvBindsTcPluginM :: TcPluginM EvBindsVar
-getEvBindsTcPluginM = fmap (expectJust oops) getEvBindsTcPluginM_maybe
-  where
-    oops = "plugin attempted to read EvBindsVar outside the constraint solver"
 #endif
index 9f94c12..6c800f4 100644 (file)
@@ -2486,18 +2486,19 @@ withTcPlugins hsc_env m =
   do plugins <- liftIO (loadTcPlugins hsc_env)
      case plugins of
        [] -> m  -- Common fast case
-       _  -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins
+       _  -> do ev_binds_var <- newTcEvBinds
+                (solvers,stops) <- unzip `fmap` mapM (startPlugin ev_binds_var) plugins
                 -- This ensures that tcPluginStop is called even if a type
                 -- error occurs during compilation (Fix of #10078)
                 eitherRes <- tryM $ do
                   updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m
-                mapM_ (flip runTcPluginM Nothing) stops
+                mapM_ (flip runTcPluginM ev_binds_var) stops
                 case eitherRes of
                   Left _ -> failM
                   Right res -> return res
   where
-  startPlugin (TcPlugin start solve stop) =
-    do s <- runTcPluginM start Nothing
+  startPlugin ev_binds_var (TcPlugin start solve stop) =
+    do s <- runTcPluginM start ev_binds_var
        return (solve s, stop s)
 
 loadTcPlugins :: HscEnv -> IO [TcPlugin]
index b871daf..ada89f1 100644 (file)
@@ -91,7 +91,7 @@ module TcRnMonad(
   -- * Type constraints
   newTcEvBinds,
   addTcEvBind,
-  getTcEvBinds, getTcEvBindsMap,
+  getTcEvTyCoVars, getTcEvBindsMap,
   chooseUniqueOccTc,
   getConstraintVar, setConstraintVar,
   emitConstraints, emitSimple, emitSimples,
@@ -1375,28 +1375,30 @@ debugTc thing
 -}
 
 newTcEvBinds :: TcM EvBindsVar
-newTcEvBinds = do { ref <- newTcRef emptyEvBindMap
+newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap
+                  ; tcvs_ref  <- newTcRef emptyVarSet
                   ; uniq <- newUnique
                   ; traceTc "newTcEvBinds" (text "unique =" <+> ppr uniq)
-                  ; return (EvBindsVar ref uniq) }
+                  ; return (EvBindsVar { ebv_binds = binds_ref
+                                       , ebv_tcvs = tcvs_ref
+                                       , ebv_uniq = uniq }) }
+
+getTcEvTyCoVars :: EvBindsVar -> TcM TyCoVarSet
+getTcEvTyCoVars (EvBindsVar { ebv_tcvs = ev_ref })
+  = readTcRef ev_ref
+
+getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap
+getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref })
+  = readTcRef ev_ref
 
 addTcEvBind :: EvBindsVar -> EvBind -> TcM ()
 -- Add a binding to the TcEvBinds by side effect
-addTcEvBind (EvBindsVar ev_ref u) ev_bind
+addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind
   = do { traceTc "addTcEvBind" $ ppr u $$
                                  ppr ev_bind
        ; bnds <- readTcRef ev_ref
        ; writeTcRef ev_ref (extendEvBinds bnds ev_bind) }
 
-getTcEvBinds :: EvBindsVar -> TcM (Bag EvBind)
-getTcEvBinds (EvBindsVar ev_ref _)
-  = do { bnds <- readTcRef ev_ref
-       ; return (evBindMapBinds bnds) }
-
-getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap
-getTcEvBindsMap (EvBindsVar ev_ref _)
-  = readTcRef ev_ref
-
 chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName
 chooseUniqueOccTc fn =
   do { env <- getGblEnv
index f5abe16..c3d1897 100644 (file)
@@ -103,6 +103,7 @@ module TcRnTypes(
         pushErrCtxt, pushErrCtxtSameOrigin,
 
         SkolemInfo(..), pprSigSkolInfo, pprSkolInfo,
+        termEvidenceAllowed,
 
         CtEvidence(..), TcEvDest(..),
         mkGivenLoc, mkKindLoc, toKindLoc,
@@ -112,7 +113,7 @@ module TcRnTypes(
         -- Constraint solver plugins
         TcPlugin(..), TcPluginResult(..), TcPluginSolver,
         TcPluginM, runTcPluginM, unsafeTcPluginTcM,
-        getEvBindsTcPluginM_maybe,
+        getEvBindsTcPluginM,
 
         CtFlavour(..), ctEvFlavour,
         CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
@@ -2150,12 +2151,8 @@ data Implication
 
       ic_wanted :: WantedConstraints,  -- The wanted
 
-      ic_binds  :: Maybe EvBindsVar,
-                                  -- Points to the place to fill in the
+      ic_binds  :: EvBindsVar,    -- Points to the place to fill in the
                                   -- abstraction and bindings.
-                                  -- is Nothing if we can't deal with
-                                  -- non-equality constraints here
-                                  -- (this happens in TcS.deferTcSForAllEq)
 
       ic_status   :: ImplicStatus
     }
@@ -2756,6 +2753,14 @@ data SkolemInfo
 instance Outputable SkolemInfo where
   ppr = pprSkolInfo
 
+termEvidenceAllowed :: SkolemInfo -> Bool
+-- Whether an implication constraint with this SkolemInfo
+-- is permitted to have term-level evidence.  There is
+-- only one that is not, associated with unifiying
+-- forall-types
+termEvidenceAllowed (UnifyForAllSkol {}) = False
+termEvidenceAllowed _                    = True
+
 pprSkolInfo :: SkolemInfo -> SDoc
 -- Complete the sentence "is a rigid type variable bound by..."
 pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty
@@ -2835,7 +2840,7 @@ data CtOrigin
                                    -- function or instance
 
   | TypeEqOrigin { uo_actual   :: TcType
-                 , uo_expected :: ExpType
+                 , uo_expected :: TcType
                  , uo_thing    :: Maybe ErrorThing
                                   -- ^ The thing that has type "actual"
                  }
@@ -3158,9 +3163,9 @@ type TcPluginSolver = [Ct]    -- given
                    -> [Ct]    -- wanted
                    -> TcPluginM TcPluginResult
 
-newtype TcPluginM a = TcPluginM (Maybe EvBindsVar -> TcM a)
+newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a)
 
-instance Functor     TcPluginM where
+instance Functor TcPluginM where
   fmap = liftM
 
 instance Applicative TcPluginM where
@@ -3178,7 +3183,7 @@ instance MonadFail.MonadFail TcPluginM where
   fail x   = TcPluginM (const $ fail x)
 #endif
 
-runTcPluginM :: TcPluginM a -> Maybe EvBindsVar -> TcM a
+runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a
 runTcPluginM (TcPluginM m) = m
 
 -- | This function provides an escape for direct access to
@@ -3190,8 +3195,8 @@ unsafeTcPluginTcM = TcPluginM . const
 -- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
 -- constraint solving.  Returns 'Nothing' if invoked during
 -- 'tcPluginInit' or 'tcPluginStop'.
-getEvBindsTcPluginM_maybe :: TcPluginM (Maybe EvBindsVar)
-getEvBindsTcPluginM_maybe = TcPluginM return
+getEvBindsTcPluginM :: TcPluginM EvBindsVar
+getEvBindsTcPluginM = TcPluginM return
 
 
 data TcPlugin = forall s. TcPlugin
index 37740bd..0174b4a 100644 (file)
@@ -41,8 +41,8 @@ module TcSMonad (
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getLclEnv,
-    getTcEvBinds, getTcEvBindsFromVar, getTcLevel,
-    getTcEvBindsMap,
+    getTcEvBindsVar, getTcLevel,
+    getTcEvBindsAndTCVs, getTcEvBindsMap,
     tcLookupClass,
 
     -- Inerts
@@ -2309,9 +2309,7 @@ should do two things differently:
 
 data TcSEnv
   = TcSEnv {
-      tcs_ev_binds    :: Maybe EvBindsVar,
-          -- this could be Nothing if we can't deal with non-equality
-          -- constraints, because, say, we're in a top-level type signature
+      tcs_ev_binds    :: EvBindsVar,
 
       tcs_unified     :: IORef Int,
          -- The number of unification variables we have filled
@@ -2325,10 +2323,6 @@ data TcSEnv
       -- See Note [Work list priorities] and
       tcs_worklist  :: IORef WorkList, -- Current worklist
 
-      tcs_used_tcvs :: IORef TyCoVarSet,
-        -- these variables were used when filling holes. Don't discard!
-        -- See also Note [Tracking redundant constraints] in TcSimplify
-
       tcs_need_deriveds :: Bool
         -- Keep solving, even if all the unsolved constraints are Derived
         -- See Note [Solving for Derived constraints]
@@ -2386,7 +2380,7 @@ traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
 runTcPluginTcS :: TcPluginM a -> TcS a
-runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBinds
+runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -2399,14 +2393,6 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                     ; n <- TcM.readTcRef ref
                                     ; TcM.writeTcRef ref (n+1) }
 
--- | Mark variables as used filling a coercion hole
-useVars :: TyCoVarSet -> TcS ()
-useVars vars = TcS $ \env -> useVarsTcM (tcs_used_tcvs env) vars
-
--- | Like 'useVars' but in the TcM monad
-useVarsTcM :: IORef TyCoVarSet -> TyCoVarSet -> TcM ()
-useVarsTcM ref vars = TcM.updTcRef ref (`unionVarSet` vars)
-
 csTraceTcS :: SDoc -> TcS ()
 csTraceTcS doc
   = wrapTcS $ csTraceTcM 1 (return doc)
@@ -2435,7 +2421,7 @@ runTcS :: TcS a                -- What to run
        -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds False (Just ev_binds_var) tcs
+       ; res <- runTcSWithEvBinds False ev_binds_var tcs
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
 
@@ -2445,14 +2431,16 @@ runTcS tcs
 runTcSDeriveds :: TcS a -> TcM a
 runTcSDeriveds tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds True (Just ev_binds_var) tcs }
+       ; runTcSWithEvBinds True ev_binds_var tcs }
 
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
-runTcSEqualities = runTcSWithEvBinds False Nothing
+runTcSEqualities thing_inside
+  = do { ev_binds_var <- TcM.newTcEvBinds
+       ; runTcSWithEvBinds False ev_binds_var thing_inside }
 
 runTcSWithEvBinds :: Bool  -- ^ keep running even if only Deriveds are left?
-                  -> Maybe EvBindsVar
+                  -> EvBindsVar
                   -> TcS a
                   -> TcM a
 runTcSWithEvBinds solve_deriveds ev_binds_var tcs
@@ -2460,15 +2448,11 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef emptyInert
        ; wl_var <- TcM.newTcRef emptyWorkList
-       ; used_var <- TcM.newTcRef emptyVarSet -- never read from, but see
-                                              -- nestImplicTcS
-
        ; let env = TcSEnv { tcs_ev_binds      = ev_binds_var
                           , tcs_unified       = unified_var
                           , tcs_count         = step_count
                           , tcs_inerts        = inert_var
                           , tcs_worklist      = wl_var
-                          , tcs_used_tcvs     = used_var
                           , tcs_need_deriveds = solve_deriveds }
 
              -- Run the computation
@@ -2479,16 +2463,15 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs
          csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count)
 
 #ifdef DEBUG
-       ; whenIsJust ev_binds_var $ \ebv ->
-         do { ev_binds <- TcM.getTcEvBinds ebv
-            ; checkForCyclicBinds ev_binds }
+       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
+       ; checkForCyclicBinds ev_binds
 #endif
 
        ; return res }
 
 #ifdef DEBUG
-checkForCyclicBinds :: Bag EvBind -> TcM ()
-checkForCyclicBinds ev_binds
+checkForCyclicBinds :: EvBindMap -> TcM ()
+checkForCyclicBinds ev_binds_map
   | null cycles
   = return ()
   | null coercion_cycles
@@ -2496,6 +2479,8 @@ checkForCyclicBinds ev_binds
   | otherwise
   = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
   where
+    ev_binds = evBindMapBinds ev_binds_map
+
     cycles :: [[EvBind]]
     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
@@ -2511,20 +2496,17 @@ checkForCyclicBinds ev_binds
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
-setEvBindsTcS :: Maybe EvBindsVar -> TcS a -> TcS a
-setEvBindsTcS m_ref (TcS thing_inside)
- = TcS $ \ env -> thing_inside (env { tcs_ev_binds = m_ref })
+setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
+setEvBindsTcS ref (TcS thing_inside)
+ = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
 
-nestImplicTcS :: Maybe EvBindsVar -> TyCoVarSet -- bound in this implication
+nestImplicTcS :: EvBindsVar
               -> TcLevel -> TcS a
-              -> TcS (a, TyCoVarSet)  -- also returns any vars used when filling
-                                      -- coercion holes (for redundant-constraint
-                                      -- tracking)
-nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside)
+              -> TcS a
+nestImplicTcS ref inner_tclvl (TcS thing_inside)
   = TcS $ \ TcSEnv { tcs_unified       = unified_var
                    , tcs_inerts        = old_inert_var
                    , tcs_count         = count
-                   , tcs_used_tcvs     = used_var
                    , tcs_need_deriveds = solve_deriveds
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
@@ -2532,35 +2514,21 @@ nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside)
                                      -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
-       ; new_used_var  <- TcM.newTcRef emptyVarSet
-       ; let nest_env = TcSEnv { tcs_ev_binds      = m_ref
+       ; let nest_env = TcSEnv { tcs_ev_binds      = ref
                                , tcs_unified       = unified_var
                                , tcs_count         = count
                                , tcs_inerts        = new_inert_var
                                , tcs_worklist      = new_wl_var
-                               , tcs_used_tcvs     = new_used_var
                                , tcs_need_deriveds = solve_deriveds }
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
 #ifdef DEBUG
        -- Perform a check that the thing_inside did not cause cycles
-       ; whenIsJust m_ref $ \ ref ->
-         do { ev_binds <- TcM.getTcEvBinds ref
-            ; checkForCyclicBinds ev_binds }
+       ; ev_binds <- TcM.getTcEvBindsMap ref
+       ; checkForCyclicBinds ev_binds
 #endif
-       ; used_tcvs <- TcM.readTcRef new_used_var
-
-       ; local_ev_vars <- case m_ref of
-           Nothing  -> return emptyVarSet
-           Just ref -> do { binds <- TcM.getTcEvBinds ref
-                          ; return $ mkVarSet $ map evBindVar $ bagToList binds }
-       ; let all_locals = bound_tcvs `unionVarSet` local_ev_vars
-             (inner_used_tcvs, outer_used_tcvs)
-               = partitionVarSet (`elemVarSet` all_locals) used_tcvs
-       ; useVarsTcM used_var outer_used_tcvs
-
-       ; return (res, inner_used_tcvs) }
+       ; return res }
 
 {- Note [Do not inherit the flat cache]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2684,21 +2652,22 @@ readTcRef ref = wrapTcS (TcM.readTcRef ref)
 updTcRef :: TcRef a -> (a->a) -> TcS ()
 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
 
-getTcEvBinds :: TcS (Maybe EvBindsVar)
-getTcEvBinds = TcS (return . tcs_ev_binds)
-
-getTcEvBindsFromVar :: EvBindsVar -> TcS (Bag EvBind)
-getTcEvBindsFromVar = wrapTcS . TcM.getTcEvBinds
+getTcEvBindsVar :: TcS EvBindsVar
+getTcEvBindsVar = TcS (return . tcs_ev_binds)
 
 getTcLevel :: TcS TcLevel
 getTcLevel = wrapTcS TcM.getTcLevel
 
+getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet)
+getTcEvBindsAndTCVs ev_binds_var
+  = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var
+                 ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
+                 ; return (bnds, tcvs) }
+
 getTcEvBindsMap :: TcS EvBindMap
 getTcEvBindsMap
-  = do { ev_binds <- getTcEvBinds
-       ; case ev_binds of
-           Just (EvBindsVar ev_ref _) -> wrapTcS $ TcM.readTcRef ev_ref
-           Nothing                    -> return emptyEvBindMap }
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
 
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
@@ -2958,10 +2927,17 @@ getEvTerm (Cached evt) = evt
 
 setEvBind :: EvBind -> TcS ()
 setEvBind ev_bind
-  = do { tc_evbinds <- getTcEvBinds
-       ; case tc_evbinds of
-           Just evb -> wrapTcS $ TcM.addTcEvBind evb ev_bind
-           Nothing  -> pprPanic "setEvBind" (ppr ev_bind) }
+  = do { evb <- getTcEvBindsVar
+       ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
+
+-- | Mark variables as used filling a coercion hole
+useVars :: TyCoVarSet -> TcS ()
+useVars vars
+  = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar
+       ; wrapTcS $
+         do { tcvs <- TcM.readTcRef ref
+            ; let tcvs' = tcvs `unionVarSet` vars
+            ; TcM.writeTcRef ref tcvs' } }
 
 -- | Equalities only
 setWantedEq :: TcEvDest -> Coercion -> TcS ()
@@ -3152,6 +3128,10 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
 
       ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
       ; env <- getLclEnv
+      ; ev_binds <- newTcEvBinds
+           -- We have nowhere to put these bindings
+           -- but TcSimplify.setImplicationStatus
+           -- checks that we don't actually use them
       ; let new_tclvl = pushTcLevel (tcl_tclvl env)
             wc        = WC { wc_simple = singleCt (mkNonCanonical ctev)
                            , wc_impl   = emptyBag
@@ -3162,7 +3142,7 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
                                , ic_given  = []
                                , ic_wanted = wc
                                , ic_status = IC_Unsolved
-                               , ic_binds  = Nothing -- no place to put binds
+                               , ic_binds  = ev_binds
                                , ic_env    = env
                                , ic_info   = skol_info }
       ; updWorkListTcS (extendWorkListImplic imp)
index d146c73..ddf0bce 100644 (file)
@@ -573,7 +573,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
-               runTcSWithEvBinds False (Just ev_binds_var) $
+               runTcSWithEvBinds False ev_binds_var $
                do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
@@ -692,7 +692,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                              , ic_given    = full_theta_vars
                              , ic_wanted   = wanted_transformed
                              , ic_status   = IC_Unsolved
-                             , ic_binds    = Just ev_binds_var
+                             , ic_binds    = ev_binds_var
                              , ic_info     = skol_info
                              , ic_env      = tc_lcl_env }
        ; emitImplication implic
@@ -1225,7 +1225,7 @@ solveImplication :: Implication    -- Wanted
 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
 -- which after trying to solve this implication we must restore to their original value
 solveImplication imp@(Implic { ic_tclvl  = tclvl
-                             , ic_binds  = m_ev_binds
+                             , ic_binds  = ev_binds_var
                              , ic_skols  = skols
                              , ic_given  = given_ids
                              , ic_wanted = wanteds
@@ -1243,8 +1243,8 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
        ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
 
          -- Solve the nested constraints
-       ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
-             <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
+       ; (no_given_eqs, given_insols, residual_wanted)
+             <- nestImplicTcS ev_binds_var tclvl $
                do { let loc    = mkGivenLoc tclvl info env
                         givens = mkGivens loc given_ids
                   ; given_insols <- solveSimpleGivens givens
@@ -1265,35 +1265,33 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
              <- floatEqualities skols no_given_eqs residual_wanted
 
        ; traceTcS "solveImplication 2"
-           (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs)
+           (ppr given_insols $$ ppr residual_wanted)
        ; let final_wanted = residual_wanted `addInsols` given_insols
 
        ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
                                                  , ic_wanted = final_wanted })
-                                            used_tcvs
 
-       ; evbinds <- TcS.getTcEvBindsMap
+       ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var
        ; traceTcS "solveImplication end }" $ vcat
              [ text "no_given_eqs =" <+> ppr no_given_eqs
              , text "floated_eqs =" <+> ppr floated_eqs
              , text "res_implic =" <+> ppr res_implic
-             , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
+             , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
+             , text "implication tvcs =" <+> ppr tcvs ]
 
        ; return (floated_eqs, res_implic) }
 
 ----------------------
-setImplicationStatus :: Implication -> TyCoVarSet  -- needed variables
-                     -> TcS (Maybe Implication)
+setImplicationStatus :: Implication -> TcS (Maybe Implication)
 -- Finalise the implication returned from solveImplication:
 --    * Set the ic_status field
 --    * Trim the ic_wanted field to remove Derived constraints
 -- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
-                                    , ic_info = info
+setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
+                                    , ic_info   = info
                                     , ic_tclvl  = tc_lvl
                                     , ic_wanted = wc
-                                    , ic_given = givens })
-                     used_tcvs
+                                    , ic_given  = givens })
  | some_insoluble
  = return $ Just $
    implic { ic_status = IC_Insoluble
@@ -1308,11 +1306,8 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
 
  | otherwise  -- Everything is solved; look at the implications
               -- See Note [Tracking redundant constraints]
- = do { ev_binds <- case m_ev_binds_var of
-                      Just (EvBindsVar ref _) -> TcS.readTcRef ref
-                      Nothing                 -> return emptyEvBindMap
-      ; let all_needs = neededEvVars ev_binds
-                                     (used_tcvs `unionVarSet` implic_needs)
+ = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var
+      ; let all_needs = neededEvVars ev_binds implic_needs
 
             dead_givens | warnRedundantGivens info
                         = filterOut (`elemVarSet` all_needs) givens
@@ -1333,9 +1328,14 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
                                                    , wc_impl   = pruned_implics } }
                -- We can only prune the child implications (pruned_implics)
                -- in the IC_Solved status case, because only then we can
-               -- accumulate their needed evidence variales into the
+               -- accumulate their needed evidence variables into the
                -- IC_Solved final_status field of the parent implication.
 
+        -- Check that there are no term-level evidence bindings
+        -- in the cases where we have no place to put them
+      ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds)
+                , ppr info $$ ppr ev_binds )
+
       ; return $ if discard_entire_implication
                  then Nothing
                  else Just final_implic }
@@ -1383,12 +1383,12 @@ warnRedundantGivens (SigSkol ctxt _)
 warnRedundantGivens (InstSkol {}) = True
 warnRedundantGivens _             = False
 
-neededEvVars :: EvBindMap -> VarSet -> VarSet
+neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet
 -- Find all the evidence variables that are "needed",
 --    and then delete all those bound by the evidence bindings
--- See note [Tracking redundant constraints]
-neededEvVars ev_binds initial_seeds
- = needed `minusVarSet` bndrs
+-- See Note [Tracking redundant constraints]
+neededEvVars (ev_binds, tcvs) initial_seeds
+ = (needed `unionVarSet` tcvs) `minusVarSet` bndrs
  where
    seeds  = foldEvBindMap add_wanted initial_seeds ev_binds
    needed = transCloVarSet also_needs seeds
@@ -1457,8 +1457,8 @@ works:
 * When the constraint solver finishes solving all the wanteds in
   an implication, it sets its status to IC_Solved
 
-  - The ics_dead field, of IC_Solved, records the subset of this implication's
-    ic_given that are redundant (not needed).
+  - The ics_dead field, of IC_Solved, records the subset of this
+    implication's ic_given that are redundant (not needed).
 
   - The ics_need field of IC_Solved then records all the
     in-scope (given) evidence variables bound by the context, that
@@ -1471,7 +1471,6 @@ works:
     a) it is free in the RHS of a Wanted EvBind,
     b) it is free in the RHS of an EvBind whose LHS is needed,
     c) it is in the ics_need of a nested implication.
-    d) it is listed in the tcs_used_tcvs field of the nested TcSEnv
 
 * We need to be careful not to discard an implication
   prematurely, even one that is fully solved, because we might
@@ -2053,8 +2052,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
   = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
        ; fake_ev_binds_var <- TcS.newTcEvBinds
        ; tclvl             <- TcS.getTcLevel
-       ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet
-                                       (pushTcLevel tclvl) try_group
+       ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
 
        ; if success then
              -- Success: record the type variable binding, and return
index 5013f47..159c6dc 100644 (file)
@@ -24,13 +24,14 @@ module TcType (
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
   TcKind, TcCoVar, TcTyCoVar, TcTyBinder, TcTyVarBinder, TcTyCon,
 
-  ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
+  ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
 
   SyntaxOpType(..), synKnownType, mkSynFunTys,
 
   -- TcLevel
   TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
   strictlyDeeperThan, sameDepthAs, fmvTcLevel,
+  tcTypeLevel, tcTyVarLevel, maxTcLevel,
 
   --------------------------------
   -- MetaDetails
@@ -40,7 +41,7 @@ module TcType (
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
   isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
   isFskTyVar, isFmvTyVar, isFlattenTyVar,
-  isAmbiguousTyVar, metaTvRef, metaTyVarInfo,
+  isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar, isTouchableOrFmv,
@@ -298,19 +299,30 @@ type TcDTyCoVarSet  = DTyCoVarSet
 -- | An expected type to check against during type-checking.
 -- See Note [ExpType] in TcMType, where you'll also find manipulators.
 data ExpType = Check TcType
-             | Infer Unique  -- for debugging only
-                     TcLevel -- See Note [TcLevel of ExpType] in TcMType
-                     Kind
-                     (IORef (Maybe TcType))
+             | Infer !InferResult
+
+data InferResult
+  = IR { ir_uniq :: Unique  -- For debugging only
+       , ir_lvl  :: TcLevel -- See Note [TcLevel of ExpType] in TcMType
+       , ir_inst :: Bool    -- True <=> deeply instantiate before returning
+                            --           i.e. return a RhoType
+                            -- False <=> do not instantaite before returning
+                            --           i.e. return a SigmaType
+       , ir_kind :: Kind
+       , ir_ref  :: IORef (Maybe TcType) }
 
 type ExpSigmaType = ExpType
 type ExpRhoType   = ExpType
 
 instance Outputable ExpType where
-  ppr (Check ty) = ppr ty
-  ppr (Infer u lvl ki _)
-    = parens (text "Infer" <> braces (ppr u <> comma <> ppr lvl)
-              <+> dcolon <+> ppr ki)
+  ppr (Check ty) = text "Check" <> braces (ppr ty)
+  ppr (Infer ir) = ppr ir
+
+instance Outputable InferResult where
+  ppr (IR { ir_uniq = u, ir_lvl = lvl
+          , ir_kind = ki, ir_inst = inst })
+    = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
+       <+> dcolon <+> ppr ki
 
 -- | Make an 'ExpType' suitable for checking.
 mkCheckExpType :: TcType -> ExpType
@@ -420,6 +432,7 @@ we would need to enforce the separation.
 -- See Note [TyVars and TcTyVars]
 data TcTyVarDetails
   = SkolemTv      -- A skolem
+       TcLevel    -- Level of the implication that binds it
        Bool       -- True <=> this skolem type variable can be overlapped
                   --          when looking up instances
                   -- See Note [Binding when looking up instances] in InstEnv
@@ -437,8 +450,8 @@ data TcTyVarDetails
 
 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
 -- See Note [Binding when looking up instances] in InstEnv
-vanillaSkolemTv = SkolemTv False  -- Might be instantiated
-superSkolemTv   = SkolemTv True   -- Treat this as a completely distinct type
+vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False  -- Might be instantiated
+superSkolemTv   = SkolemTv (pushTcLevel topTcLevel) True   -- Treat this as a completely distinct type
 
 -----------------------------
 data MetaDetails
@@ -467,10 +480,10 @@ instance Outputable MetaDetails where
 
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
-pprTcTyVarDetails (SkolemTv True)  = text "ssk"
-pprTcTyVarDetails (SkolemTv False) = text "sk"
 pprTcTyVarDetails (RuntimeUnk {})  = text "rt"
 pprTcTyVarDetails (FlatSkol {})    = text "fsk"
+pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
+pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
   = pp_info <> colon <> ppr tclvl
   where
@@ -655,6 +668,9 @@ We arrange the TcLevels like this
 The flatten meta-vars are all at level 0, just to make them untouchable.
 -}
 
+maxTcLevel :: TcLevel -> TcLevel -> TcLevel
+maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
+
 fmvTcLevel :: TcLevel -> TcLevel
 -- See Note [TcLevel assignment]
 fmvTcLevel _ = TcLevel 0
@@ -685,6 +701,24 @@ checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
 checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
   = ctxt_tclvl >= tv_tclvl
 
+tcTyVarLevel :: TcTyVar -> TcLevel
+tcTyVarLevel tv
+  = ASSERT2( isTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+          MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
+          SkolemTv tv_lvl _             -> tv_lvl
+          FlatSkol ty                   -> tcTypeLevel ty
+          RuntimeUnk                    -> topTcLevel
+
+tcTypeLevel :: TcType -> TcLevel
+-- Max level of any free var of the type
+tcTypeLevel ty
+  = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
+  where
+    add v lvl
+      | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
+      | otherwise   = lvl
+
 instance Outputable TcLevel where
   ppr (TcLevel us) = ppr us
 
@@ -1034,8 +1068,8 @@ isSkolemTyVar tv
 isOverlappableTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-        SkolemTv overlappable -> overlappable
-        _                     -> False
+        SkolemTv overlappable -> overlappable
+        _                       -> False
 
 isMetaTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
@@ -1076,6 +1110,12 @@ metaTyVarTcLevel_maybe tv
       MetaTv { mtv_tclvl = tclvl } -> Just tclvl
       _                            -> Nothing
 
+metaTyVarRef :: TyVar -> IORef MetaDetails
+metaTyVarRef tv
+  = case tcTyVarDetails tv of
+        MetaTv { mtv_ref = ref } -> ref
+        _ -> pprPanic "metaTyVarRef" (ppr tv)
+
 setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar
 setMetaTyVarTcLevel tv tclvl
   = case tcTyVarDetails tv of
@@ -1088,12 +1128,6 @@ isSigTyVar tv
         MetaTv { mtv_info = SigTv } -> True
         _                           -> False
 
-metaTvRef :: TyVar -> IORef MetaDetails
-metaTvRef tv
-  = case tcTyVarDetails tv of
-        MetaTv { mtv_ref = ref } -> ref
-        _ -> pprPanic "metaTvRef" (ppr tv)
-
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
 isFlexi _     = False
index 2712c4a..4b0b749 100644 (file)
@@ -6,23 +6,23 @@
 Type subsumption and unification
 -}
 
-{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
+{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
 
 module TcUnify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
-  tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
-  tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC,
+  tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
+  tcSubTypeDS_NC_O, tcSubTypeET,
   checkConstraints, buildImplicationFor,
 
   -- Various unifications
   unifyType, unifyTheta, unifyKind, noThing,
-  uType, unifyExpType,
+  uType,
   swapOverTyVars, canSolveByUnification,
 
   --------------------------------
   -- Holes
-  tcInfer,
+  tcInferInst, tcInferNoInst,
   matchExpectedListTy,
   matchExpectedPArrTy,
   matchExpectedTyConApp,
@@ -112,14 +112,15 @@ passed in.
 -}
 
 -- Use this one when you have an "expected" type.
-matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchExpectedFunTys :: forall a.
+                       SDoc   -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
                     -> ExpRhoType  -- deeply skolemised
                     -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
                           -- must fill in these ExpTypes here
                     -> TcM (a, HsWrapper)
 -- If    matchExpectedFunTys n ty = (_, wrap)
--- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty,
+-- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
 --   where [t1, ..., tn], ty_r are passed to the thing_inside
 matchExpectedFunTys herald arity orig_ty thing_inside
   = case orig_ty of
@@ -166,14 +167,16 @@ matchExpectedFunTys herald arity orig_ty thing_inside
                           defer acc_arg_tys n (mkCheckExpType ty)
 
     ------------
+    defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
     defer acc_arg_tys n fun_ty
-      = do { more_arg_tys <- replicateM n newOpenInferExpType
-           ; res_ty       <- newOpenInferExpType
+      = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
+           ; res_ty       <- newInferExpTypeInst
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM readExpType more_arg_tys
            ; res_ty       <- readExpType res_ty
            ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
-           ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty
+           ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
+                         -- Not a good origin at all :-(
            ; return (result, wrap) }
 
     ------------
@@ -198,7 +201,7 @@ matchActualFunTys :: Outputable a
                   -> TcSigmaType
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
 -- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
--- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
+-- then  wrap : ty ~> (t1 -> ... -> tn -> ty_r)
 matchActualFunTys herald ct_orig mb_thing arity ty
   = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
 
@@ -523,82 +526,36 @@ tcSubTypeHR :: Outputable a
             -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
-tcSubType :: Outputable a
-          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
-          -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
--- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
-tcSubType ctxt maybe_thing ty_actual ty_expected
-  = tcSubTypeO origin ctxt ty_actual ty_expected
-  where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
-
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
-tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET orig ty_actual ty_expected
-  = uExpTypeX orig ty_expected ty_actual
-              (return . mkWpCastN . mkTcSymCo)
-              (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a
-                                    (mkCheckExpType ty_expected))
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
--- Does not add context.
-tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected
-  = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual
-tcSubTypeET_NC ctxt (Check ty_actual) ty_expected
-  = tc_sub_type orig orig ctxt ty_actual ty_expected'
+------------------------
+tcSubTypeET :: CtOrigin -> UserTypeCtxt
+            -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type_et t1 t2
+--    => wrap :: t1 ~> t2
+tcSubTypeET orig ctxt (Check ty_actual) ty_expected
+  = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
   where
-    ty_expected' = mkCheckExpType ty_expected
-    orig = TypeEqOrigin { uo_actual   = ty_actual
-                        , uo_expected = ty_expected'
-                        , uo_thing    = Nothing }
+    eq_orig = TypeEqOrigin { uo_actual   = ty_expected
+                           , uo_expected = ty_actual
+                           , uo_thing    = Nothing }
 
+tcSubTypeET _ _ (Infer inf_res) ty_expected
+  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
+    do { co <- fillInferResult ty_expected inf_res
+       ; return (mkWpCastN (mkTcSymCo co)) }
+
+------------------------
 tcSubTypeO :: CtOrigin      -- ^ of the actual type
            -> UserTypeCtxt  -- ^ of the expected type
            -> TcSigmaType
-           -> ExpSigmaType
+           -> ExpRhoType
            -> TcM HsWrapper
-tcSubTypeO origin ctxt ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    do { traceTc "tcSubType" (vcat [ pprCtOrigin origin
-                                   , pprUserTypeCtxt ctxt
-                                   , ppr ty_actual
-                                   , ppr ty_expected ])
-       ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected }
-  where
-    eq_orig | TypeEqOrigin {} <- origin = origin
-            | otherwise
-            = TypeEqOrigin { uo_actual   = ty_actual
-                           , uo_expected = ty_expected
-                           , uo_thing    = Nothing }
-
-tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
-            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised (hence "DS")
-tcSubTypeDS ctxt m_expr ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected
-
--- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
--- the "actual" type
-tcSubTypeDS_O :: Outputable a
-              => CtOrigin -> UserTypeCtxt
-              -> Maybe a -> TcSigmaType -> ExpRhoType
-              -> TcM HsWrapper
-tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
+tcSubTypeO orig ctxt ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -628,26 +585,24 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
 -- The "_NC" variants do not add a typechecker-error context;
 -- the caller is assumed to do that
 
-tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
+tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- Checks that actual <= expected
+-- Returns HsWrapper :: actual ~ expected
 tcSubType_NC ctxt ty_actual ty_expected
   = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
+       ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected }
   where
     origin = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
                           , uo_thing    = Nothing }
 
-tcSubTypeDS_NC :: Outputable a
-               => UserTypeCtxt
-               -> Maybe a  -- ^ If present, this has type ty_actual
-               -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
-tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
-  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
-  where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
+tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
+-- Just like tcSubType, but with the additional precondition that
+-- ty_expected is deeply skolemised (hence "DS")
+tcSubTypeDS orig ctxt ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
+       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
 
 tcSubTypeDS_NC_O :: Outputable a
                  => CtOrigin   -- origin used for instantiation only
@@ -656,56 +611,72 @@ tcSubTypeDS_NC_O :: Outputable a
                  -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
-tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual)
-  where
-    eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et
-                           , uo_thing = mkErrorThing <$> m_thing }
+tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
+  = case ty_expected of
+      Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res
+      Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
+         where
+           eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
+                                  , uo_thing = mkErrorThing <$> m_thing }
 
 ---------------
-tc_sub_type :: CtOrigin   -- origin used when calling uType
-            -> CtOrigin   -- origin used when instantiating
-            -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
-tc_sub_type eq_orig inst_orig ctxt ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual)
-
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
                -> CtOrigin   -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type t1 t2
+--    => wrap :: t1 ~> t2
 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
-  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
-  = do { lookup_res <- lookupTcTyVar tv_actual
-       ; case lookup_res of
-           Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig
-                                               ctxt ty_actual' ty_expected
-
-             -- It's tempting to see if tv_actual can unify with a polytype
-             -- and, if so, call uType; otherwise, skolemise first. But this
-             -- is wrong, because skolemising will bump the TcLevel and the
-             -- unification will fail anyway.
-             -- It's also tempting to call uUnfilledVar directly, but calling
-             -- uType seems safer in the presence of possible refactoring
-             -- later.
-           Unfilled _        -> mkWpCastN <$>
-                                uType eq_orig TypeLevel ty_actual ty_expected }
-
-  | otherwise  -- See Note [Deep skolemisation]
-  = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
-                                  \ _ sk_rho ->
+  | is_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
+  , not (is_poly ty_actual)
+  = do { traceTc "tc_sub_tc_type (drop to equality)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; mkWpCastN <$>
+         uType eq_orig TypeLevel ty_actual ty_expected }
+
+  | otherwise   -- This is the general case
+  = do { traceTc "tc_sub_tc_type (general case)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
+                                                   \ _ sk_rho ->
                                   tc_sub_type_ds eq_orig inst_orig ctxt
                                                  ty_actual sk_rho
        ; return (sk_wrap <.> inner_wrap) }
+  where
+    is_poly ty
+      | isForAllTy ty                        = True
+      | Just (_, res) <- splitFunTy_maybe ty = is_poly res
+      | otherwise                            = False
+      -- NB *not* tcSplitFunTy, because here we want
+      -- to decompose type-class arguments too
+
+
+{- Note [Don't skolemise unnecessarily]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to solve
+    (Char->Char) <= (forall a. a->a)
+We could skolemise the 'forall a', and then complain
+that (Char ~ a) is insoluble; but that's a pretty obscure
+error.  It's better to say that
+    (Char->Char) ~ (forall a. a->a)
+fails.
+
+In general,
+ * if the RHS type an outermost forall (i.e. skolemisation
+   is the next thing we'd do)
+ * and the LHS has no top-level polymorphism (but looking deeply)
+then we can revert to simple equality.
+-}
 
 ---------------
 tc_sub_type_ds :: CtOrigin    -- used when calling uType
                -> CtOrigin    -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised
+-- If wrap = tc_sub_type_ds t1 t2
+--    => wrap :: t1 ~> t2
+-- Here is where the work actually happens!
+-- Precondition: ty_expected is deeply skolemised
 tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
   = go ty_actual ty_expected
   where
@@ -739,8 +710,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                                           (SigSkol GenSigCtxt exp_arg))
                                  ctxt exp_arg act_arg
            ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
-               -- arg_wrap :: exp_arg ~ act_arg
-               -- res_wrap :: act-res ~ exp_res
+               -- arg_wrap :: exp_arg ~> act_arg
+               -- res_wrap :: act-res ~> exp_res
 
     go ty_a ty_e
       | let (tvs, theta, _) = tcSplitSigmaTy ty_a
@@ -748,8 +719,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
       = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
            ; body_wrap <- tc_sub_type_ds
                             (eq_orig { uo_actual = in_rho
-                                     , uo_expected =
-                                         mkCheckExpType ty_expected })
+                                     , uo_expected = ty_expected })
                             inst_orig ctxt in_rho ty_e
            ; return (body_wrap <.> in_wrap) }
 
@@ -815,23 +785,124 @@ wrapFunResCoercion arg_tys co_fn_res
   = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
         ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
 
------------------------------------
+
+{- **********************************************************************
+%*                                                                      *
+            ExpType functions: tcInfer, fillInferResult
+%*                                                                      *
+%********************************************************************* -}
+
 -- | Infer a type using a fresh ExpType
 -- See also Note [ExpType] in TcMType
-tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_check
-  = do { res_ty <- newOpenInferExpType
+-- Does not attempt to instantiate the inferred type
+tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInferNoInst = tcInfer False
+
+tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
+tcInferInst = tcInfer True
+
+tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer instantiate tc_check
+  = do { res_ty <- newInferExpType instantiate
        ; result <- tc_check res_ty
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-{-
-************************************************************************
+fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = fillInferResult_Inst t1 t2
+--    => wrap :: t1 ~> t2
+-- See Note [Deep instantiation of InferResult]
+fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me })
+  | instantiate_me
+  = do { (wrap, rho) <- deeplyInstantiate orig ty
+       ; co <- fillInferResult rho inf_res
+       ; return (mkWpCastN co <.> wrap) }
+
+  | otherwise
+  = do { co <- fillInferResult ty inf_res
+       ; return (mkWpCastN co) }
+
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fillInferResult t1 t2
+--    => wrap :: t1 ~> t2
+fillInferResult ty (IR { ir_uniq = u, ir_lvl = res_lvl
+                       , ir_kind = res_kind, ir_ref = ref })
+  = do { (ty_co, ty) <- promoteTcType res_lvl ty
+       ; ki_co <- uType kind_orig KindLevel ty_kind res_kind
+       ; let ty_to_fill_with = ty `mkCastTy` ki_co
+             co = ty_co `mkTcCoherenceRightCo` ki_co
+
+       ; when debugIsOn (check_hole ty_to_fill_with)
+
+       ; traceTc "Filling ExpType" $
+         ppr u <+> text ":=" <+> ppr ty_to_fill_with
+
+       ; writeTcRef ref (Just ty)
+
+       ; return co }
+  where
+    ty_kind = typeKind ty
+    kind_orig = TypeEqOrigin { uo_actual   = ty_kind
+                             , uo_expected = res_kind
+                             , uo_thing    = Nothing }
+
+    check_hole ty   -- Debug check only
+      = do { ki1 <- zonkTcType (typeKind ty)
+           ; ki2 <- zonkTcType res_kind
+           ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
+           ; let ty_lvl = tcTypeLevel ty
+           ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
+                       ppr u $$ ppr res_lvl $$ ppr ty_lvl )
+           ; cts <- readTcRef ref
+           ; case cts of
+               Just already_there -> pprPanic "writeExpType"
+                                       (vcat [ ppr u
+                                             , ppr ty
+                                             , ppr already_there ])
+               Nothing -> return () }
+
+{- Note [Deep instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some cases we want to deeply instantiate before filling in
+an InferResult, and in some cases not.  That's why InferReult
+has the ir_inst flag.
+
+* ir_inst = True: deeply instantantiate
+
+  Consider
+    f x = (*)
+  We want to instantiate the type of (*) before returning, else we
+  will infer the type
+    f :: forall {a}. a -> forall b. Num b => b -> b -> b
+  This is surely confusing for users.
+
+  And worse, the the monomorphism restriction won't properly. The MR is
+  dealt with in simplifyInfer, and simplifyInfer has no way of
+  instantiating. This could perhaps be worked around, but it may be
+  hard to know even when instantiation should happen.
+
+  Another reason.  Consider
+       f :: (?x :: Int) => a -> a
+       g y = let ?x = 3::Int in f
+  Here want to instantiate f's type so that the ?x::Int constraint
+  gets discharged by the enclosing implicit-parameter binding.
+
+* ir_inst = False: do not instantantiate
+
+  Consider this (which uses visible type application):
+
+    (let { f :: forall a. a -> a; f x = x } in f) @Int
+
+  We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
+  And we don't want to instantite the type of 'f' when we reach it,
+  else the outer visible type application won't work
+-}
+
+{- *********************************************************************
 *                                                                      *
-\subsection{Generalisation}
+                    Generalisation
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 -- | Take an "expected type" and strip off quantifiers to expose the
 -- type underneath, binding the new skolems for the @thing_inside@.
@@ -949,7 +1020,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
                              , ic_given = given
                              , ic_wanted = wanted
                              , ic_status  = IC_Unsolved
-                             , ic_binds = Just ev_binds_var
+                             , ic_binds = ev_binds_var
                              , ic_env = env
                              , ic_info = skol_info }
 
@@ -972,19 +1043,9 @@ unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
 -- Returns a coercion : ty1 ~ ty2
 unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
   where
-    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
+    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
                           , uo_thing  = mkErrorThing <$> thing }
 
--- | Variant of 'unifyType' that takes an 'ExpType' as its second type
-unifyExpType :: Outputable a => Maybe a
-             -> TcTauType -> ExpType -> TcM TcCoercionN
-unifyExpType mb_thing ty1 ty2
-  = uExpType ty_orig ty1 ty2
-  where
-    ty_orig   = TypeEqOrigin { uo_actual   = ty1
-                             , uo_expected = ty2
-                             , uo_thing    = mkErrorThing <$> mb_thing }
-
 -- | Use this instead of 'Nothing' when calling 'unifyType' without
 -- a good "thing" (where the "thing" has the "actual" type passed in)
 -- This has an 'Outputable' instance, avoiding amgiguity problems.
@@ -993,7 +1054,7 @@ noThing = Nothing
 
 unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
 unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
-  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
+  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
                               , uo_thing  = mkErrorThing <$> thing }
 
 ---------------
@@ -1020,34 +1081,6 @@ unifyTheta theta1 theta2
 uType is the heart of the unifier.
 -}
 
-uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN
-uExpType orig ty1 et
-  = uExpTypeX orig ty1 et return $
-    uType orig TypeLevel ty1
-
--- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first
--- continuation with the produced coercion. Otherwise, calls the second
--- continuation. This can happen either with a Check or with an untouchable
--- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType]
-uExpTypeX :: CtOrigin -> TcType -> ExpType
-          -> (TcCoercionN -> TcM a)   -- Infer case, co :: TcType ~N ExpType
-          -> (TcType -> TcM a)        -- Check / untouchable case
-          -> TcM a
-uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont
-  = do { cur_lvl <- getTcLevel
-       ; if cur_lvl `sameDepthAs` tc_lvl
-         then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki
-                 ; writeExpType et (ty1 `mkCastTy` ki_co)
-                 ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co }
-         else do { traceTc "Preventing writing to untouchable ExpType" empty
-                 ; tau <- expTypeToType et -- See Note [TcLevel of ExpType]
-                 ; type_cont tau }}
-  where
-    kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel)
-uExpTypeX _ _ (Check ty2) _ type_cont
-  = type_cont ty2
-
-------------
 uType, uType_defer
   :: CtOrigin
   -> TypeOrKind
@@ -1059,23 +1092,18 @@ uType, uType_defer
 -- It is always safe to defer unification to the main constraint solver
 -- See Note [Deferred unification]
 uType_defer origin t_or_k ty1 ty2
-  = do { hole <- newCoercionHole
-       ; loc <- getCtLocM origin (Just t_or_k)
-       ; emitSimple $ mkNonCanonical $
-             CtWanted { ctev_dest = HoleDest hole
-                      , ctev_pred = mkPrimEqPred ty1 ty2
-                      , ctev_loc = loc }
+  = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
 
        -- Error trace only
-       -- NB. do *not* call mkErrInfo unless tracing is on, because
-       -- it is hugely expensive (#5631)
+       -- NB. do *not* call mkErrInfo unless tracing is on,
+       --     because it is hugely expensive (#5631)
        ; whenDOptM Opt_D_dump_tc_trace $ do
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1,
+            ; traceTc "utype_defer" (vcat [ppr co, ppr ty1,
                                            ppr ty2, pprCtOrigin origin, doc])
             }
-       ; return (mkHoleCo hole Nominal ty1 ty2) }
+       ; return co }
 
 --------------
 uType origin t_or_k orig_ty1 orig_ty2
@@ -1667,9 +1695,330 @@ matchExpectedFunKind num_args_remaining ty = go
            ; let new_fun = mkFunTy arg_kind res_kind
                  thing   = mkTypeErrorThingArgs ty num_args_remaining
                  origin  = TypeEqOrigin { uo_actual   = k
-                                        , uo_expected = mkCheckExpType new_fun
+                                        , uo_expected = new_fun
                                         , uo_thing    = Just thing
                                         }
            ; co <- uType origin KindLevel k new_fun
            ; return (co, arg_kind, res_kind) }
-      where
+
+
+{- *********************************************************************
+*                                                                      *
+                 Occurrence checking
+*                                                                      *
+********************************************************************* -}
+
+
+{- Note [Occurs check expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
+of occurrences of tv outside type function arguments, if that is
+possible; otherwise, it returns Nothing.
+
+For example, suppose we have
+  type F a b = [a]
+Then
+  occCheckExpand b (F Int b) = Just [Int]
+but
+  occCheckExpand a (F a Int) = Nothing
+
+We don't promise to do the absolute minimum amount of expanding
+necessary, but we try not to do expansions we don't need to.  We
+prefer doing inner expansions first.  For example,
+  type F a b = (a, Int, a, [a])
+  type G b   = Char
+We have
+  occCheckExpand b (F (G b)) = Just (F Char)
+even though we could also expand F to get rid of b.
+
+The two variants of the function are to support TcUnify.checkTauTvUpdate,
+which wants to prevent unification with type families. For more on this
+point, see Note [Prevent unification with type families] in TcUnify.
+
+Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are considering unifying
+   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
+This may be an error (what is that alpha doing inside beta's kind?),
+but we must not make the mistake of actuallyy unifying or we'll
+build an infinite data structure.  So when looking for occurrences
+of alpha in the rhs, we must look in the kinds of type variables
+that occur there.
+
+NB: we may be able to remove the problem via expansion; see
+    Note [Occurs check expansion].  So we have to try that.
+
+Note [Checking for foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unless we have -XImpredicativeTypes (which is a totally unsupported
+feature), we do not want to unify
+    alpha ~ (forall a. a->a) -> Int
+So we look for foralls hidden inside the type, and it's convenient
+to do that at the same time as the occurs check (which looks for
+occurrences of alpha).
+
+However, it's not just a question of looking for foralls /anywhere/!
+Consider
+   (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
+This is legal; e.g. dependent/should_compile/T11635.
+
+We don't want to reject it because of the forall in beta's kind,
+but (see Note [Occurrence checking: look inside kinds]) we do
+need to look in beta's kind.  So we carry a flag saying if a 'forall'
+is OK, and sitch the flag on when stepping inside a kind.
+
+Why is it OK?  Why does it not count as impredicative polymorphism?
+The reason foralls are bad is because we reply on "seeing" foralls
+when doing implicit instantiation.  But the forall inside the kind is
+fine.  We'll generate a kind equality constraint
+  (forall k. k->*) ~ (forall k. k->*)
+to check that the kinds of lhs and rhs are compatible.  If alpha's
+kind had instead been
+  (alpha :: kappa)
+then this kind equality would rightly complain about unifying kappa
+with (forall k. k->*)
+
+-}
+
+data OccCheckResult a
+  = OC_OK a
+  | OC_Bad     -- Forall or type family
+  | OC_Occurs
+
+instance Functor OccCheckResult where
+      fmap = liftM
+
+instance Applicative OccCheckResult where
+      pure = OC_OK
+      (<*>) = ap
+
+instance Monad OccCheckResult where
+  OC_OK x    >>= k = k x
+  OC_Bad     >>= _ = OC_Bad
+  OC_Occurs  >>= _ = OC_Occurs
+
+occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
+-- Just for error-message generation; so we return OccCheckResult
+-- so the caller can report the right kind of error
+-- Check whether
+--   a) the given variable occurs in the given type.
+--   b) there is a forall in the type (unless we have -XImpredicativeTypes)
+occCheckForErrors dflags tv ty
+  = case preCheck dflags True tv ty of
+      OC_OK _   -> OC_OK ()
+      OC_Bad    -> OC_Bad
+      OC_Occurs -> case occCheckExpand tv ty of
+                     Nothing -> OC_Occurs
+                     Just _  -> OC_OK ()
+
+----------------
+metaTyVarUpdateOK :: DynFlags
+                  -> TcTyVar             -- tv :: k1
+                  -> TcType              -- ty :: k2
+                  -> Maybe TcType        -- possibly-expanded ty
+-- (metaTyFVarUpdateOK tv ty)
+-- We are about to update the meta-tyvar tv with ty, in
+-- our on-the-flyh unifier
+-- Check (a) that tv doesn't occur in ty (occurs check)
+--       (b) that ty does not have any foralls
+--           (in the impredicative case), or type functions
+--
+-- We have two possible outcomes:
+-- (1) Return the type to update the type variable with,
+--        [we know the update is ok]
+-- (2) Return Nothing,
+--        [the update might be dodgy]
+--
+-- Note that "Nothing" does not mean "definite error".  For example
+--   type family F a
+--   type instance F Int = Int
+-- consider
+--   a ~ F a
+-- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
+-- we return Nothing, leaving it to the later constraint simplifier to
+-- sort matters out.
+--
+-- See Note [Refactoring hazard: checkTauTvUpdate]
+
+metaTyVarUpdateOK dflags tv ty
+  = case preCheck dflags False tv ty of
+         -- False <=> type families not ok
+         -- See Note [Prevent unification with type families]
+      OC_OK _   -> Just ty
+      OC_Bad    -> Nothing  -- forall or type function
+      OC_Occurs -> occCheckExpand tv ty
+
+preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
+-- A quick check for
+--   (a) a forall type (unless -XImpredivativeTypes)
+--   (b) a type family
+--   (c) an occurrence of the type variable (occurs check)
+--
+-- For (a) and (b) we check only the top level of the type, NOT
+-- inside the kinds of variables it mentions.  But for (c) we do
+-- look in the kinds of course.
+
+preCheck dflags ty_fam_ok tv ty
+  = fast_check ty
+  where
+    details          = tcTyVarDetails tv
+    impredicative_ok = canUnifyWithPolyType dflags details
+
+    ok :: OccCheckResult ()
+    ok = OC_OK ()
+
+    fast_check :: TcType -> OccCheckResult ()
+    fast_check (TyVarTy tv')
+      | tv == tv' = OC_Occurs
+      | otherwise = fast_check_occ (tyVarKind tv')
+           -- See Note [Occurrence checking: look inside kinds]
+
+    fast_check (TyConApp tc tys)
+      | bad_tc tc              = OC_Bad
+      | otherwise              = mapM fast_check tys >> ok
+    fast_check (LitTy {})      = ok
+    fast_check (FunTy a r)     = fast_check a   >> fast_check r
+    fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
+    fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
+    fast_check (CoercionTy co) = fast_check_co co
+    fast_check (ForAllTy (TvBndr tv' _) ty)
+       | not impredicative_ok = OC_Bad
+       | tv == tv'            = ok
+       | otherwise = do { fast_check_occ (tyVarKind tv')
+                        ; fast_check_occ ty }
+       -- Under a forall we look only for occurrences of
+       -- the type variable
+
+     -- For kinds, we only do an occurs check; we do not worry
+     -- about type families or foralls
+     -- See Note [Checking for foralls]
+    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
+                     | otherwise                        = ok
+
+     -- For coercions, we are only doing an occurs check here;
+     -- no bother about impredicativity in coercions, as they're
+     -- inferred
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+                     | otherwise                       = ok
+
+    bad_tc :: TyCon -> Bool
+    bad_tc tc
+      | not (impredicative_ok || isTauTyCon tc)     = True
+      | not (ty_fam_ok        || isFamFreeTyCon tc) = True
+      | otherwise                                   = False
+
+occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
+-- See Note [Occurs check expansion]
+-- We may have needed to do some type synonym unfolding in order to
+-- get rid of the variable (or forall), so we also return the unfolded
+-- version of the type, which is guaranteed to be syntactically free
+-- of the given type variable.  If the type is already syntactically
+-- free of the variable, then the same type is returned.
+occCheckExpand tv ty
+  = go emptyVarEnv ty
+  where
+    go :: VarEnv TyVar -> Type -> Maybe Type
+          -- The VarEnv carries mappings necessary
+          -- because of kind expansion
+    go env (TyVarTy tv')
+      | tv == tv'                         = Nothing
+      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
+      | otherwise                         = do { k' <- go env (tyVarKind tv')
+                                               ; return (mkTyVarTy $
+                                                         setTyVarKind tv' k') }
+           -- See Note [Occurrence checking: look inside kinds]
+
+    go _   ty@(LitTy {}) = return ty
+    go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
+                                ; ty2' <- go env ty2
+                                ; return (mkAppTy ty1' ty2') }
+    go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
+                                ; ty2' <- go env ty2
+                                ; return (mkFunTy ty1' ty2') }
+    go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
+       | tv == tv'         = return ty
+       | otherwise         = do { ki' <- go env (tyVarKind tv')
+                                ; let tv'' = setTyVarKind tv' ki'
+                                      env' = extendVarEnv env tv' tv''
+                                ; body' <- go env' body_ty
+                                ; return (ForAllTy (TvBndr tv'' vis) body') }
+
+    -- For a type constructor application, first try expanding away the
+    -- offending variable from the arguments.  If that doesn't work, next
+    -- see if the type constructor is a type synonym, and if so, expand
+    -- it and try again.
+    go env ty@(TyConApp tc tys)
+      = case mapM (go env) tys of
+          Just tys' -> return (mkTyConApp tc tys')
+          Nothing | Just ty' <- coreView ty -> go env ty'
+                  | otherwise               -> Nothing
+                      -- Failing that, try to expand a synonym
+
+    go env (CastTy ty co) =  do { ty' <- go env ty
+                                ; co' <- go_co env co
+                                ; return (mkCastTy ty' co') }
+    go env (CoercionTy co) = do { co' <- go_co env co
+                                ; return (mkCoercionTy co') }
+
+    ------------------
+    go_co env (Refl r ty)               = do { ty' <- go env ty
+                                             ; return (mkReflCo r ty') }
+      -- Note: Coercions do not contain type synonyms
+    go_co env (TyConAppCo r tc args)    = do { args' <- mapM (go_co env) args
+                                             ; return (mkTyConAppCo r tc args') }
+    go_co env (AppCo co arg)            = do { co' <- go_co env co
+                                             ; arg' <- go_co env arg
+                                             ; return (mkAppCo co' arg') }
+    go_co env co@(ForAllCo tv' kind_co body_co)
+      | tv == tv'         = return co
+      | otherwise         = do { kind_co' <- go_co env kind_co
+                               ; let tv'' = setTyVarKind tv' $
+                                            pFst (coercionKind kind_co')
+                                     env' = extendVarEnv env tv' tv''
+                               ; body' <- go_co env' body_co
+                               ; return (ForAllCo tv'' kind_co' body') }
+    go_co env (CoVarCo c)               = do { k' <- go env (varType c)
+                                             ; return (mkCoVarCo (setVarType c k')) }
+    go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
+                                             ; return (mkAxiomInstCo ax ind args') }
+    go_co env (UnivCo p r ty1 ty2)      = do { p' <- go_prov env p
+                                             ; ty1' <- go env ty1
+                                             ; ty2' <- go env ty2
+                                             ; return (mkUnivCo p' r ty1' ty2') }
+    go_co env (SymCo co)                = do { co' <- go_co env co
+                                             ; return (mkSymCo co') }
+    go_co env (TransCo co1 co2)         = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkTransCo co1' co2') }
+    go_co env (NthCo n co)              = do { co' <- go_co env co
+                                             ; return (mkNthCo n co') }
+    go_co env (LRCo lr co)              = do { co' <- go_co env co
+                                             ; return (mkLRCo lr co') }
+    go_co env (InstCo co arg)           = do { co' <- go_co env co
+                                             ; arg' <- go_co env arg
+                                             ; return (mkInstCo co' arg') }
+    go_co env (CoherenceCo co1 co2)     = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkCoherenceCo co1' co2') }
+    go_co env (KindCo co)               = do { co' <- go_co env co
+                                             ; return (mkKindCo co') }
+    go_co env (SubCo co)                = do { co' <- go_co env co
+                                             ; return (mkSubCo co') }
+    go_co env (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co env) cs
+                                             ; return (mkAxiomRuleCo ax cs') }
+
+    ------------------
+    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
+    go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
+    go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
+    go_prov _   p@(PluginProv _)    = return p
+    go_prov _   p@(HoleProv _)      = return p
+
+canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
+canUnifyWithPolyType dflags details
+  = case details of
+      MetaTv { mtv_info = SigTv }    -> False
+      MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
+      _other                         -> True
+          -- We can have non-meta tyvars in given constraints
+
index 49767fe..31859e1 100644 (file)
@@ -206,7 +206,7 @@ checkAmbiguity ctxt ty
        ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
        ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
                             captureConstraints $
-                            tcSubType_NC ctxt ty (mkCheckExpType ty)
+                            tcSubType_NC ctxt ty ty
        ; simplifyAmbiguityCheck ty wanted
 
        ; traceTc "Done ambiguity check for" (ppr ty) }
index 1765ff5..bf92c37 100644 (file)
@@ -1270,11 +1270,13 @@ splitForAllTyVarBndrs ty = split ty ty []
 
 -- | Checks whether this is a proper forall (with a named binder)
 isForAllTy :: Type -> Bool
+isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty'
 isForAllTy (ForAllTy {}) = True
 isForAllTy _             = False
 
 -- | Is this a function or forall?
 isPiTy :: Type -> Bool
+isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
 isPiTy (ForAllTy {}) = True
 isPiTy (FunTy {})    = True
 isPiTy _             = False
index d4abeae..e5b94b1 100644 (file)
@@ -44,7 +44,7 @@ buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst
 buildDataFamInst name' fam_tc vect_tc rhs
  = do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
 
-      ; (_, tyvars') <- liftDs $ tcInstSigTyVars (getSrcSpan name') tyvars
+      ; (_, tyvars') <- liftDs $ freshenTyVarBndrs tyvars
       ; let ax       = mkSingleCoAxiom Representational axiom_name tyvars' [] fam_tc pat_tys rep_ty
             tys'     = mkTyVarTys tyvars'
             rep_ty   = mkTyConApp rep_tc tys'
index 20f04d0..6f9e16f 100644 (file)
@@ -30,9 +30,9 @@ TYPE SIGNATURES
     (Num t, Monad m) =>
     (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
   test6 ::
-    forall a (m :: * -> *) t.
+    forall a (m :: * -> *) p.
     (Num (m a), Monad m) =>
-    (m a -> m (m a)) -> t -> m a
+    (m a -> m (m a)) -> p -> m a
 TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
index 6782f27..6e7732f 100644 (file)
@@ -1,8 +1,8 @@
 
 annfail10.hs:9:1: error:
-    • Ambiguous type variable ‘t0’ arising from an annotation
-      prevents the constraint ‘(Data.Data.Data t0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘t0’ should be.
+    • Ambiguous type variable ‘p0’ arising from an annotation
+      prevents the constraint ‘(Data.Data.Data p0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instances exist:
         instance (Data.Data.Data a, Data.Data.Data b) =>
                  Data.Data.Data (Either a b)
@@ -15,9 +15,9 @@ annfail10.hs:9:1: error:
     • In the annotation: {-# ANN f 1 #-}
 
 annfail10.hs:9:11: error:
-    • Ambiguous type variable ‘t0’ arising from the literal ‘1’
-      prevents the constraint ‘(Num t0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘t0’ should be.
+    • Ambiguous type variable ‘p0’ arising from the literal ‘1’
+      prevents the constraint ‘(Num p0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instances exist:
         instance Num Integer -- Defined in ‘GHC.Num’
         instance Num Double -- Defined in ‘GHC.Float’
index b5a5f1d..770135a 100644 (file)
@@ -1,24 +1,24 @@
 
 T2182.hs:5:5: error:
-    No instance for (Show (t1 -> t1)) arising from a use of ‘show’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: show (\ x -> x)
-    In an equation for ‘y’: y = show (\ x -> x)
+    • No instance for (Show (p1 -> p1)) arising from a use of ‘show’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: show (\ x -> x)
+      In an equation for ‘y’: y = show (\ x -> x)
 
 T2182.hs:6:5: error:
-    No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: (\ x -> x) == (\ y -> y)
-    In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
+    • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: (\ x -> x) == (\ y -> y)
+      In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
 
 T2182.hs:5:5: error:
-    No instance for (Show (t1 -> t1)) arising from a use of ‘show’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: show (\ x -> x)
-    In an equation for ‘y’: y = show (\ x -> x)
+    • No instance for (Show (p1 -> p1)) arising from a use of ‘show’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: show (\ x -> x)
+      In an equation for ‘y’: y = show (\ x -> x)
 
 T2182.hs:6:5: error:
-    No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: (\ x -> x) == (\ y -> y)
-    In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
+    • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: (\ x -> x) == (\ y -> y)
+      In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
index 056d451..41322f9 100644 (file)
@@ -1,19 +1,19 @@
 
 gadt-escape1.hs:19:58: error:
-    • Couldn't match type ‘t’ with ‘ExpGADT Int’
-        ‘t’ is untouchable
-          inside the constraints: t1 ~ Int
+    • Couldn't match type ‘p’ with ‘ExpGADT Int’
+        ‘p’ is untouchable
+          inside the constraints: t ~ Int
           bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
                    in a case alternative
           at gadt-escape1.hs:19:43-50
-      ‘t’ is a rigid type variable bound by
-        the inferred type of weird1 :: t at gadt-escape1.hs:19:1-58
+      ‘p’ is a rigid type variable bound by
+        the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58
       Possible fix: add a type signature for ‘weird1’
-      Expected type: t
-        Actual type: ExpGADT t1
+      Expected type: p
+        Actual type: ExpGADT t
     • In the expression: a
       In a case alternative: Hidden (ExpInt _) a -> a
       In the expression:
         case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
     • Relevant bindings include
-        weird1 :: t (bound at gadt-escape1.hs:19:1)
+        weird1 :: p (bound at gadt-escape1.hs:19:1)
index e304430..6673ff6 100644 (file)
@@ -1,17 +1,17 @@
 
 gadt13.hs:15:13: error:
-    • Couldn't match expected type ‘t
+    • Couldn't match expected type ‘p
                   with actual type ‘String -> [Char]’
-        ‘t’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
-      ‘t’ is a rigid type variable bound by
-        the inferred type of shw :: Term a -> t at gadt13.hs:15:1-30
+      ‘p’ is a rigid type variable bound by
+        the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30
       Possible fix: add a type signature for ‘shw’
     • Possible cause: ‘(.)’ is applied to too many arguments
       In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
-        shw :: Term a -> t (bound at gadt13.hs:15:1)
+        shw :: Term a -> p (bound at gadt13.hs:15:1)
index e66226e..f75e8c5 100644 (file)
@@ -1,20 +1,20 @@
 
 gadt7.hs:16:38: error:
-    • Couldn't match expected type ‘t’ with actual type ‘t1’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘p1’
+        ‘p1’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘t’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
+      ‘p’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
       In the expression: case t1 of { K -> y1 }
     • Relevant bindings include
-        y1 :: t1 (bound at gadt7.hs:16:16)
-        y :: t1 (bound at gadt7.hs:16:7)
-        i1b :: T a -> t1 -> t (bound at gadt7.hs:16:1)
+        y1 :: p1 (bound at gadt7.hs:16:16)
+        y :: p1 (bound at gadt7.hs:16:7)
+        i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1)
index 904f0cd..2e86b42 100644 (file)
@@ -1,14 +1,14 @@
 Stopped in Main.g, break012.hs:5:10-18
-_result :: (t, a1 -> a1, (), a -> a -> a) = _
-a :: t = _
+_result :: (p, a1 -> a1, (), a -> a -> a) = _
+a :: p = _
 b :: a2 -> a2 = _
 c :: () = _
 d :: a -> a -> a = _
-a :: t
+a :: p
 b :: a2 -> a2
 c :: ()
 d :: a -> a -> a
-a = (_t1::t)
+a = (_t1::p)
 b = (_t2::a2 -> a2)
 c = (_t3::())
 d = (_t4::a -> a -> a)
index 40d2b59..5d81c04 100644 (file)
@@ -2,7 +2,7 @@
 test = C 1 32 1.2 1.23 'x' 1 1.2 1.23
 Breakpoint 0 activated at print022.hs:11:7
 Stopped in Main.f, print022.hs:11:7
-_result :: t = _
-x :: t = _
+_result :: p = _
+x :: p = _
 x = C2 1 (W# 32) (TwoFields 'a' 3)
 x :: T2
index 164e0cf..2712257 100644 (file)
@@ -2,7 +2,7 @@ without -fprint-explicit-foralls
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 pattern P :: Bool      -- Defined at <interactive>:16:1
 pattern Pe :: a -> Ex  -- Defined at <interactive>:17:1
-pattern Pu :: t -> t   -- Defined at <interactive>:18:1
+pattern Pu :: p -> p   -- Defined at <interactive>:18:1
 pattern Pue :: a -> a1 -> (a, Ex)      -- Defined at <interactive>:19:1
 pattern Pur :: (Num a, Eq a) => a -> [a]
        -- Defined at <interactive>:20:1
@@ -26,7 +26,7 @@ with -fprint-explicit-foralls
 pattern P :: Bool      -- Defined at <interactive>:16:1
 pattern Pe :: () => forall {a}. a -> Ex
        -- Defined at <interactive>:17:1
-pattern Pu :: forall {t}. t -> t       -- Defined at <interactive>:18:1
+pattern Pu :: forall {p}. p -> p       -- Defined at <interactive>:18:1
 pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
        -- Defined at <interactive>:19:1
 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
index 8a8d3dd..5f60194 100644 (file)
@@ -1,25 +1,25 @@
 
 <interactive>:2:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:10:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:19:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:28:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:49:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/indexed-types/should_fail/T12386.hs b/testsuite/tests/indexed-types/should_fail/T12386.hs
new file mode 100644 (file)
index 0000000..c07881a
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T12386 where
+
+class C a where
+   type family F a t :: *
+
+   type family T a :: *
+   type T a = F a
diff --git a/testsuite/tests/indexed-types/should_fail/T12386.stderr b/testsuite/tests/indexed-types/should_fail/T12386.stderr
new file mode 100644 (file)
index 0000000..66d812e
--- /dev/null
@@ -0,0 +1,7 @@
+
+T12386.hs:9:15: error:
+    • Expecting one more argument to ‘F a’
+      Expected a type, but ‘F a’ has kind ‘* -> *’
+    • In the type ‘F a’
+      In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
index f1ae705..9cc8912 100644 (file)
@@ -1,13 +1,15 @@
 
-T5439.hs:82:28: error:
-    • Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’
-                     with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
-      Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
-        Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
-    • In the first argument of ‘complete’, namely ‘ev’
-      In the expression: complete ev
+T5439.hs:82:33: error:
+    • Couldn't match expected type ‘Attempt (HElemOf rs)’
+                  with actual type ‘Attempt (HHead (HDrop n0 l0))
+                                    -> Attempt (HElemOf l0)’
+    • In the second argument of ‘($)’, namely
+        ‘inj $ Failure (e :: SomeException)’
       In a stmt of a 'do' block:
         c <- complete ev $ inj $ Failure (e :: SomeException)
+      In the expression:
+        do { c <- complete ev $ inj $ Failure (e :: SomeException);
+             return $ c || not first }
     • Relevant bindings include
         register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
           (bound at T5439.hs:64:9)
index 0332181..b7b70b8 100644 (file)
@@ -1,11 +1,11 @@
 
 T7354.hs:28:11: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ Base t1 (Prim [t] t)
-      Expected type: Prim [t] t -> Base t1 (Prim [t] t)
-        Actual type: Prim [t] t -> t
+        p ~ Base t (Prim [p] p)
+      Expected type: Prim [p] p -> Base t (Prim [p] p)
+        Actual type: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’
       In the expression: ana alg
       In an equation for ‘foo’: foo = ana alg
     • Relevant bindings include
-        foo :: Prim [t] t -> t1 (bound at T7354.hs:28:1)
+        foo :: Prim [p] p -> t (bound at T7354.hs:28:1)
index 09e79ee..228672b 100644 (file)
@@ -1,7 +1,7 @@
 
 read014.hs:4:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      ng1 :: Num a => t -> a -> a
+      ng1 :: Num a => p -> a -> a
 
 read014.hs:4:5: warning: [-Wunused-matches (in -Wextra)]
     Defined but not used: ‘x’
index f7617ee..fe949d9 100644 (file)
@@ -1,10 +1,7 @@
 
 T7848.hs:6:1: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ t0 -> t1 -> A -> A -> A -> A -> t2 -> t
-    • When checking that:
-          t0 -> t1 -> A -> A -> A -> A -> forall t2. t2 -> t
-        is more polymorphic than: t
+        t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t
     • Relevant bindings include x :: t (bound at T7848.hs:6:1)
 
 T7848.hs:10:9: error:
index 963bc50..2dca583 100644 (file)
@@ -1,7 +1,7 @@
 
 readFail003.hs:4:27: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ (t, [a1], [a])
+        a2 ~ (a2, [a1], [a])
     • In the expression: a
       In a pattern binding:
         ~(a, b, c)
@@ -11,6 +11,6 @@ readFail003.hs:4:27: error:
           where
               nullity = null
     • Relevant bindings include
-        a :: t (bound at readFail003.hs:4:3)
+        a :: a2 (bound at readFail003.hs:4:3)
         b :: [a1] (bound at readFail003.hs:4:5)
         c :: [a] (bound at readFail003.hs:4:7)
index ebf2a75..c5238bb 100644 (file)
@@ -1,8 +1,8 @@
 
 T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t2’
-      Where: ‘t2’ is a rigid type variable bound by
-               the inferred type of g :: t2 -> t2 at T10438.hs:(6,9)-(8,21)
+    • Found type wildcard ‘_’ standing for ‘p2’
+      Where: ‘p2’ is a rigid type variable bound by
+               the inferred type of g :: p2 -> p2 at T10438.hs:(6,9)-(8,21)
     • In the type signature: x :: _
       In an equation for ‘g’:
           g r
@@ -20,7 +20,7 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
                       x :: _
                       x = r
     • Relevant bindings include
-        r :: t2 (bound at T10438.hs:6:11)
-        g :: t2 -> t2 (bound at T10438.hs:6:9)
-        f :: t1 (bound at T10438.hs:5:5)
-        foo :: t1 -> forall t. t -> t (bound at T10438.hs:5:1)
+        r :: p2 (bound at T10438.hs:6:11)
+        g :: p2 -> p2 (bound at T10438.hs:6:9)
+        f :: p1 (bound at T10438.hs:5:5)
+        foo :: p1 -> p -> p (bound at T10438.hs:5:1)
index 7abf6e5..8e47c4b 100644 (file)
@@ -1,8 +1,8 @@
 
 T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Int -> t -> t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of go :: Int -> t -> t at T11192.hs:8:8-17
+    • Found type wildcard ‘_’ standing for ‘Int -> p -> p
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of go :: Int -> p -> p at T11192.hs:8:8-17
     • In the type signature: go :: _
       In the expression:
         let
@@ -18,11 +18,11 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Relevant bindings include fails :: a (bound at T11192.hs:6:1)
 
 T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t1 -> t -> t
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
-             ‘t’ is a rigid type variable bound by
-               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
+    • Found type wildcard ‘_’ standing for ‘p1 -> p -> p
+      Where: ‘p1’ is a rigid type variable bound by
+               the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17
+             ‘p’ is a rigid type variable bound by
+               the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17
     • In the type signature: go :: _
       In the expression:
         let
index 9c438dd..838d75c 100644 (file)
@@ -8,7 +8,7 @@ T11213.hs:20:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:21:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
-      pattern Pu :: forall t. t -> t
+      pattern Pu :: forall p. p -> p
 
 T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
index 20714e7..8f370ce 100644 (file)
@@ -1,8 +1,8 @@
 
 mono.hs:7:4: error:
     • Couldn't match type ‘Bool’ with ‘Int’
-      Expected type: [Int]
-        Actual type: [Bool]
+      Expected type: [Bool]
+        Actual type: [Int]
     • In the pattern: Single x
       In an equation for ‘f’: f (Single x) = x
 
index 9f8f62e..7a079ff 100644 (file)
@@ -1,19 +1,19 @@
 
 T7438.hs:6:14: error:
-    • Couldn't match expected type ‘t’ with actual type ‘t1’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘p1’
+        ‘p1’ is untouchable
           inside the constraints: b ~ a
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
-      ‘t’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
-        acc :: t1 (bound at T7438.hs:6:8)
-        go :: Thrist a b -> t1 -> t (bound at T7438.hs:6:1)
+        acc :: p1 (bound at T7438.hs:6:8)
+        go :: Thrist a b -> p1 -> p (bound at T7438.hs:6:1)
index 241cf76..712724d 100644 (file)
@@ -25,15 +25,15 @@ rebindable6.hs:110:17: error:
                    return b }
 
 rebindable6.hs:111:17: error:
-    • Ambiguous type variables ‘t1’, ‘t0’ arising from a do statement
+    • Ambiguous type variables ‘p0’, ‘t0’ arising from a do statement
       prevents the constraint ‘(HasBind
-                                  (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved.
+                                  (IO (Maybe b) -> (Maybe b -> p0) -> t0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘t1’, ‘t0’ should be.
+      Probable fix: use a type annotation to specify what ‘p0’, ‘t0’ should be.
       These potential instance exist:
         instance HasBind (IO a -> (a -> IO b) -> IO b)
           -- Defined at rebindable6.hs:51:18
@@ -49,15 +49,15 @@ rebindable6.hs:111:17: error:
                    return b }
 
 rebindable6.hs:112:17: error:
-    • Ambiguous type variable ‘t1’ arising from a use of ‘return’
-      prevents the constraint ‘(HasReturn (b -> t1))’ from being solved.
+    • Ambiguous type variable ‘p0’ arising from a use of ‘return’
+      prevents the constraint ‘(HasReturn (b -> p0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
         b :: b (bound at rebindable6.hs:111:23)
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘t1’ should be.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instance exist:
         instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:46:18
     • In a stmt of a 'do' block: return b
index 8364fd0..e3df440 100644 (file)
@@ -1,3 +1,3 @@
 
 T12597.hs:5:1: warning: [-Wmissing-signatures (in -Wall)]
-    Top-level binding with no type signature: f :: t -> t
+    Top-level binding with no type signature: f :: p -> p
index 9826868..df20e67 100644 (file)
@@ -65,7 +65,8 @@ AbsBinds [a] []
    Exported types: T8958.$fRepresentationala [InlPrag=[ALWAYS] CONLIKE]
                      :: forall a. Representational a
                    [LclIdX[DFunId],
-                    Unf=DFun: \ (@ a[ssk]) -> T8958.C:Representational TYPE: a[ssk]]
+                    Unf=DFun: \ (@ a[ssk:2]) ->
+                          T8958.C:Representational TYPE: a[ssk:2]]
    Binds: $dRepresentational = T8958.C:Representational @ a
    Evidence: [EvBinds{}]}
 AbsBinds [a] []
@@ -74,7 +75,7 @@ AbsBinds [a] []
    Exported types: T8958.$fNominala [InlPrag=[ALWAYS] CONLIKE]
                      :: forall a. Nominal a
                    [LclIdX[DFunId],
-                    Unf=DFun: \ (@ a[ssk]) -> T8958.C:Nominal TYPE: a[ssk]]
+                    Unf=DFun: \ (@ a[ssk:2]) -> T8958.C:Nominal TYPE: a[ssk:2]]
    Binds: $dNominal = T8958.C:Nominal @ a
    Evidence: [EvBinds{}]}
 
index cecaad1..b100172 100644 (file)
@@ -1,7 +1,7 @@
 
 ==================== Pre unarise: ====================
 Noinline01.f [InlPrag=INLINE (sat-args=1)]
-  :: forall t. t -> GHC.Types.Bool
+  :: forall p. p -> GHC.Types.Bool
 [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] =
     \r [eta] GHC.Types.True [];
 
@@ -26,7 +26,7 @@ Noinline01.$trModule :: GHC.Types.Module
 
 ==================== STG syntax: ====================
 Noinline01.f [InlPrag=INLINE (sat-args=1)]
-  :: forall t. t -> GHC.Types.Bool
+  :: forall p. p -> GHC.Types.Bool
 [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] =
     \r [eta] GHC.Types.True [];
 
index f59fcbd..32064a9 100644 (file)
@@ -7,7 +7,7 @@ T11452.hs:6:14: error:
       In an equation for ‘impred’: impred = $$([|| \ _ -> () ||])
 
 T11452.hs:6:14: error:
-    • Cannot instantiate unification variable ‘t0’
+    • Cannot instantiate unification variable ‘p0’
       with a type involving foralls: forall a. a -> a
         GHC doesn't yet support impredicative polymorphism
     • In the Template Haskell quotation [|| \ _ -> () ||]
index 4ddf100..3265a5e 100644 (file)
@@ -1,4 +1,4 @@
-inside b: t_0
+inside b: p_0
 inside d: GHC.Types.Bool
 type of c: GHC.Types.Bool
 inside f: GHC.Types.Bool
index 696bff7..6cc24fc 100644 (file)
@@ -1,6 +1,6 @@
 
 ExPatFail.hs:12:15: error:
-    • Couldn't match expected type ‘t’ with actual type ‘a’
+    • Couldn't match expected type ‘p’ with actual type ‘a’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         a pattern with constructor:
@@ -11,4 +11,4 @@ ExPatFail.hs:12:15: error:
       In a pattern binding: MkT y _ = x
       In the expression: let MkT y _ = x in y
     • Relevant bindings include
-        f :: T -> t (bound at ExPatFail.hs:12:1)
+        f :: T -> p (bound at ExPatFail.hs:12:1)
diff --git a/testsuite/tests/typecheck/should_compile/T12427.stderr b/testsuite/tests/typecheck/should_compile/T12427.stderr
new file mode 100644 (file)
index 0000000..0519ecb
--- /dev/null
@@ -0,0 +1 @@
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr
new file mode 100644 (file)
index 0000000..fc2aece
--- /dev/null
@@ -0,0 +1,33 @@
+
+T12427a.hs:17:29: error:
+    • Couldn't match expected type ‘p’
+                  with actual type ‘(forall b. [b] -> [b]) -> Int’
+        ‘p’ is untouchable
+          inside the constraints: ()
+          bound by a pattern with constructor:
+                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
+                   in a case alternative
+          at T12427a.hs:17:19-24
+      ‘p’ is a rigid type variable bound by
+        the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
+      Possible fix: add a type signature for ‘h11’
+    • In the expression: v
+      In a case alternative: T1 _ v -> v
+      In the expression: case y of { T1 _ v -> v }
+    • Relevant bindings include
+        h11 :: T -> p (bound at T12427a.hs:17:1)
+
+T12427a.hs:28:6: error:
+    • Couldn't match expected type ‘p’
+                  with actual type ‘(forall b. [b] -> [b]) -> Int’
+        ‘p’ is untouchable
+          inside the constraints: ()
+          bound by a pattern with constructor:
+                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
+                   in a pattern binding
+          at T12427a.hs:28:1-7
+      ‘p’ is a rigid type variable bound by
+        the inferred type of x1 :: p at T12427a.hs:28:1-19
+      Possible fix: add a type signature for ‘x1’
+    • In the pattern: T1 _ x1
+      In a pattern binding: T1 _ x1 = undefined
index d205fa9..7d0f081 100644 (file)
@@ -35,7 +35,7 @@ tc141.hs:13:13: error:
         in v
 
 tc141.hs:15:18: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘t
+    • Couldn't match expected type ‘a2’ with actual type ‘p
         because type variable ‘a2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
@@ -50,5 +50,5 @@ tc141.hs:15:18: error:
         in v
     • Relevant bindings include
         v :: a2 (bound at tc141.hs:15:14)
-        b :: t (bound at tc141.hs:13:5)
-        g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1)
+        b :: p (bound at tc141.hs:13:5)
+        g :: a1 -> p -> a (bound at tc141.hs:13:1)
index e09e60a..5067d25 100644 (file)
@@ -1,8 +1,8 @@
 
-T10495.hs:5:1: error:
+T10495.hs:5:7: error:
     • Couldn't match representation of type ‘a0’ with that of ‘b0’
         arising from a use of ‘coerce’
-    • When instantiating ‘foo’, initially inferred to have
-      this overly-general type:
-        forall a b. Coercible a b => a -> b
-      NB: This instantiation can be caused by the monomorphism restriction.
+    • In the expression: coerce
+      In an equation for ‘foo’: foo = coerce
+    • Relevant bindings include
+        foo :: a0 -> b0 (bound at T10495.hs:5:1)
index 7a27229..fde2daf 100644 (file)
@@ -17,7 +17,7 @@ T10619.hs:9:15: error:
               else
                   \ y -> y
     • Relevant bindings include
-        foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
+        foo :: p -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
 
 T10619.hs:14:15: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
@@ -37,7 +37,7 @@ T10619.hs:14:15: error:
               else
                   ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
     • Relevant bindings include
-        bar :: t -> (b -> b) -> b -> b (bound at T10619.hs:12:1)
+        bar :: p -> (b -> b) -> b -> b (bound at T10619.hs:12:1)
 
 T10619.hs:16:13: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
index 48bf94d..03c885a 100644 (file)
@@ -2,27 +2,24 @@
 T12177.hs:3:19: error:
     • Found hole: _ :: t
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t2 -> t1 -> t
-               at T12177.hs:3:1-19
+               the inferred type of bar :: p1 -> p -> t at T12177.hs:3:1-19
     • In the expression: _
       In the expression: \ x -> _
       In the expression: \ x -> \ x -> _
     • Relevant bindings include
-        x :: t1 (bound at T12177.hs:3:14)
-        bar :: t2 -> t1 -> t (bound at T12177.hs:3:1)
+        x :: p (bound at T12177.hs:3:14)
+        bar :: p1 -> p -> t (bound at T12177.hs:3:1)
 
 T12177.hs:5:37: error:
     • Found hole: _ :: t
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t
+               the inferred type of baz :: p4 -> p3 -> p2 -> p1 -> p -> t
                at T12177.hs:5:1-37
     • In the expression: _
       In the expression: \ z -> _
       In the expression: \ x -> \ z -> _
     • Relevant bindings include
-        z :: t1 (bound at T12177.hs:5:32)
-        x :: t2 (bound at T12177.hs:5:26)
-        y :: t4 (bound at T12177.hs:5:14)
-        baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t
-          (bound at T12177.hs:5:1)
-          
\ No newline at end of file
+        z :: p (bound at T12177.hs:5:32)
+        x :: p1 (bound at T12177.hs:5:26)
+        y :: p3 (bound at T12177.hs:5:14)
+        baz :: p4 -> p3 -> p2 -> p1 -> p -> t (bound at T12177.hs:5:1)
index dd5abb2..910ac06 100644 (file)
@@ -1,5 +1,5 @@
 {-# OPTIONS -XImplicitParams -XRankNTypes #-}
- module Bug where
+module Bug where
 
 t :: forall a. ((?p :: Int) => a) -> String
 t _ = "Hello"
@@ -10,3 +10,7 @@ f _ = 3
 result :: Int
 result = f t
 
+
+-- This should work.
+-- Elaborated result = f (/\a. \x:a. t @a (\p::Int. x))
+-- But it did not work in 8.0.1; fixed in HEAD
index 66979dd..e69de29 100644 (file)
@@ -1,12 +0,0 @@
-
-T3102.hs:11:12: error:
-    • Couldn't match type ‘a’ with ‘(?p::Int) => a0’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. a -> String
-        at T3102.hs:11:10-12
-      Expected type: a -> String
-        Actual type: ((?p::Int) => a0) -> String
-    • In the first argument of ‘f’, namely ‘t’
-      In the expression: f t
-      In an equation for ‘result’: result = f t
index 6b8e920..9157e11 100644 (file)
@@ -1,13 +1,13 @@
 
 T7453.hs:9:15: error:
-    • Couldn't match type ‘t’ with ‘t1
-        because type variable ‘t1’ would escape its scope
+    • Couldn't match type ‘p’ with ‘t
+        because type variable ‘t’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: Id t1
+          z :: Id t
         at T7453.hs:8:11-19
-      Expected type: Id t1
-        Actual type: Id t
+      Expected type: Id t
+        Actual type: Id p
     • In the expression: aux
       In an equation for ‘z’:
           z = aux
@@ -22,20 +22,20 @@ T7453.hs:9:15: error:
                   where
                       aux = Id v
     • Relevant bindings include
-        aux :: Id t (bound at T7453.hs:10:21)
-        z :: Id t1 (bound at T7453.hs:9:11)
-        v :: t (bound at T7453.hs:7:7)
-        cast1 :: t -> a (bound at T7453.hs:7:1)
+        aux :: Id p (bound at T7453.hs:10:21)
+        z :: Id t (bound at T7453.hs:9:11)
+        v :: p (bound at T7453.hs:7:7)
+        cast1 :: p -> a (bound at T7453.hs:7:1)
 
 T7453.hs:15:15: error:
-    • Couldn't match type ‘t1’ with ‘t2
-        because type variable ‘t2’ would escape its scope
+    • Couldn't match type ‘p’ with ‘t1
+        because type variable ‘t1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: () -> t2
+          z :: () -> t1
         at T7453.hs:14:11-22
-      Expected type: () -> t2
-        Actual type: () -> t1
+      Expected type: () -> t1
+        Actual type: () -> p
     • In the expression: aux
       In an equation for ‘z’:
           z = aux
@@ -50,17 +50,17 @@ T7453.hs:15:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t1 (bound at T7453.hs:16:21)
-        z :: () -> t2 (bound at T7453.hs:15:11)
-        v :: t1 (bound at T7453.hs:13:7)
-        cast2 :: t1 -> t (bound at T7453.hs:13:1)
+        aux :: forall b. b -> p (bound at T7453.hs:16:21)
+        z :: () -> t1 (bound at T7453.hs:15:11)
+        v :: p (bound at T7453.hs:13:7)
+        cast2 :: p -> t (bound at T7453.hs:13:1)
 
 T7453.hs:21:15: error:
-    • Couldn't match expected type ‘t2’ with actual type ‘t1
-        because type variable ‘t2’ would escape its scope
+    • Couldn't match expected type ‘t1’ with actual type ‘p
+        because type variable ‘t1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: t2
+          z :: t1
         at T7453.hs:20:11-16
     • In the expression: v
       In an equation for ‘z’:
@@ -76,7 +76,7 @@ T7453.hs:21:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t1 (bound at T7453.hs:22:21)
-        z :: t2 (bound at T7453.hs:21:11)
-        v :: t1 (bound at T7453.hs:19:7)
-        cast3 :: t1 -> forall t. t (bound at T7453.hs:19:1)
+        aux :: forall b. b -> p (bound at T7453.hs:22:21)
+        z :: t1 (bound at T7453.hs:21:11)
+        v :: p (bound at T7453.hs:19:7)
+        cast3 :: p -> t (bound at T7453.hs:19:1)
index 8553fdb..a39b048 100644 (file)
@@ -1,18 +1,18 @@
 
 T7734.hs:4:13: error:
-    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
+    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘f’: x `f` y = x x
     • Relevant bindings include
-        x :: t2 -> t1 (bound at T7734.hs:4:1)
-        f :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:4:3)
+        x :: t1 -> t (bound at T7734.hs:4:1)
+        f :: (t1 -> t) -> p -> t (bound at T7734.hs:4:3)
 
 T7734.hs:5:13: error:
-    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
+    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘&’: (&) x y = x x
     • Relevant bindings include
-        x :: t2 -> t1 (bound at T7734.hs:5:5)
-        (&) :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:5:1)
+        x :: t1 -> t (bound at T7734.hs:5:5)
+        (&) :: (t1 -> t) -> p -> t (bound at T7734.hs:5:1)
index ce1b09d..f30c49b 100644 (file)
@@ -1,14 +1,14 @@
 
 T9109.hs:8:13: error:
-    • Couldn't match expected type ‘t’ with actual type ‘Bool’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘Bool’
+        ‘p’ is untouchable
           inside the constraints: a ~ Bool
           bound by a pattern with constructor: GBool :: G Bool,
                    in an equation for ‘foo’
           at T9109.hs:8:5-9
-      ‘t’ is a rigid type variable bound by
-        the inferred type of foo :: G a -> t at T9109.hs:8:1-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: G a -> p at T9109.hs:8:1-16
       Possible fix: add a type signature for ‘foo’
     • In the expression: True
       In an equation for ‘foo’: foo GBool = True
-    • Relevant bindings include foo :: G a -> t (bound at T9109.hs:8:1)
+    • Relevant bindings include foo :: G a -> p (bound at T9109.hs:8:1)
index 218ae97..c637788 100644 (file)
@@ -1,7 +1,7 @@
 
-T9318.hs:12:5:
-    Couldn't match type ‘Char’ with ‘Bool
-    Expected type: F Int
-      Actual type: Char
-    In the pattern: 'x'
-    In an equation for ‘bar’: bar 'x' = ()
+T9318.hs:12:5: error:
+    • Couldn't match type ‘Bool’ with ‘Char
+      Expected type: F Int
+        Actual type: Char
+    • In the pattern: 'x'
+      In an equation for ‘bar’: bar 'x' = ()
index ff90a73..17486df 100644 (file)
@@ -13,7 +13,7 @@ VtaFail.hs:12:26: error:
           answer_constraint_fail = addOne @Bool 5
 
 VtaFail.hs:14:17: error:
-    • Cannot apply expression of type ‘t1 -> t1
+    • Cannot apply expression of type ‘p0 -> p0
       to a visible type argument ‘Int’
     • In the expression: (\ x -> x) @Int 12
       In an equation for ‘answer_lambda’:
index 98c57e8..4f2dbc4 100644 (file)
@@ -208,7 +208,7 @@ test('T2806', normal, compile_fail, [''])
 test('T3323', normal, compile_fail, [''])
 test('T3406', normal, compile_fail, [''])
 test('T3540', normal, compile_fail, [''])
-test('T3102', normal, compile_fail, [''])
+test('T3102', normal, compile, [''])
 test('T3613', normal, compile_fail, [''])
 test('fd-loop', normal, compile_fail, [''])
 test('T3950', normal, compile_fail, [''])
index 6755636..d72a340 100644 (file)
@@ -1,8 +1,8 @@
 
 tcfail002.hs:4:7: error:
-    • Occurs check: cannot construct the infinite type: t ~ [t]
+    • Occurs check: cannot construct the infinite type: p ~ [p]
     • In the expression: z
       In an equation for ‘c’: c z = z
     • Relevant bindings include
-        z :: [t] (bound at tcfail002.hs:4:3)
-        c :: [t] -> t (bound at tcfail002.hs:3:1)
+        z :: [p] (bound at tcfail002.hs:4:3)
+        c :: [p] -> p (bound at tcfail002.hs:3:1)
index 41a55c1..7bf64d8 100644 (file)
@@ -1,9 +1,9 @@
 
 tcfail004.hs:3:9: error:
-    • Couldn't match expected type ‘(t1, t)’
+    • Couldn't match expected type ‘(a, b)’
                   with actual type ‘(Integer, Integer, Integer)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
-        f :: t1 (bound at tcfail004.hs:3:2)
-        g :: t (bound at tcfail004.hs:3:4)
+        f :: a (bound at tcfail004.hs:3:2)
+        g :: b (bound at tcfail004.hs:3:4)
index 77437cf..56db4cf 100644 (file)
@@ -1,9 +1,9 @@
 
 tcfail005.hs:3:9: error:
-    • Couldn't match expected type ‘[t]’
+    • Couldn't match expected type ‘[a]’
                   with actual type ‘(Integer, Char)’
     • In the expression: (1, 'a')
       In a pattern binding: (h : i) = (1, 'a')
     • Relevant bindings include
-        h :: t (bound at tcfail005.hs:3:2)
-        i :: [t] (bound at tcfail005.hs:3:4)
+        h :: a (bound at tcfail005.hs:3:2)
+        i :: [a] (bound at tcfail005.hs:3:4)
index f3e815b..3803d9c 100644 (file)
@@ -4,4 +4,4 @@ tcfail013.hs:4:3: error:
     • In the pattern: True
       In an equation for ‘f’: f True = 2
     • Relevant bindings include
-        f :: [a] -> t (bound at tcfail013.hs:3:1)
+        f :: [a] -> p (bound at tcfail013.hs:3:1)
index a186fb1..f506bff 100644 (file)
@@ -1,9 +1,9 @@
 
 tcfail014.hs:5:33: error:
-    • Occurs check: cannot construct the infinite type: t7 ~ t7 -> t8
+    • Occurs check: cannot construct the infinite type: t4 ~ t4 -> t5
     • In the first argument of ‘z’, namely ‘z’
       In the expression: z z
       In an equation for ‘h’: h z = z z
     • Relevant bindings include
-        z :: t7 -> t8 (bound at tcfail014.hs:5:27)
-        h :: (t7 -> t8) -> t8 (bound at tcfail014.hs:5:25)
+        z :: t4 -> t5 (bound at tcfail014.hs:5:27)
+        h :: (t4 -> t5) -> t5 (bound at tcfail014.hs:5:25)
index 57060a8..d5594c7 100644 (file)
@@ -1,5 +1,5 @@
 
 tcfail018.hs:5:10: error:
-    • No instance for (Num [t0]) arising from the literal ‘1’
+    • No instance for (Num [a0]) arising from the literal ‘1’
     • In the expression: 1
       In a pattern binding: (a : []) = 1
index 583e6e3..d2912b2 100644 (file)
@@ -1,6 +1,6 @@
 
 tcfail032.hs:14:8: error:
-    • Couldn't match expected type ‘a1 -> Int’ with actual type ‘t
+    • Couldn't match expected type ‘a1 -> Int’ with actual type ‘p
         because type variable ‘a1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         an expression type signature:
@@ -9,5 +9,5 @@ tcfail032.hs:14:8: error:
     • In the expression: (x :: (Eq a) => a -> Int)
       In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int)
     • Relevant bindings include
-        x :: t (bound at tcfail032.hs:14:3)
-        f :: t -> forall a. Eq a => a -> Int (bound at tcfail032.hs:14:1)
+        x :: p (bound at tcfail032.hs:14:3)
+        f :: p -> a -> Int (bound at tcfail032.hs:14:1)
index f3908f3..bc30866 100644 (file)
@@ -1,6 +1,6 @@
 
 tcfail099.hs:9:20: error:
-    • Couldn't match expected type ‘a’ with actual type ‘t
+    • Couldn't match expected type ‘a’ with actual type ‘p
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         a pattern with constructor: C :: forall a. (a -> Int) -> DS,
@@ -10,6 +10,6 @@ tcfail099.hs:9:20: error:
       In the expression: f arg
       In an equation for ‘call’: call (C f) arg = f arg
     • Relevant bindings include
-        arg :: t (bound at tcfail099.hs:9:12)
+        arg :: p (bound at tcfail099.hs:9:12)
         f :: a -> Int (bound at tcfail099.hs:9:9)
-        call :: DS -> t -> Int (bound at tcfail099.hs:9:1)
+        call :: DS -> p -> Int (bound at tcfail099.hs:9:1)
index a0a6595..44d8e48 100644 (file)
@@ -3,15 +3,15 @@ tcfail104.hs:14:12: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘Char -> Char’
       Expected type: (Char -> Char) -> Char -> Char
         Actual type: (forall a. a -> a) -> Char -> Char
-    • When checking that: (forall a. a -> a) -> forall a. a -> a
-        is more polymorphic than: (Char -> Char) -> Char -> Char
-      In the expression: (\ (x :: forall a. a -> a) -> x)
+    • In the expression: (\ (x :: forall a. a -> a) -> x)
       In the expression:
         if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+      In the expression:
+        (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
 
 tcfail104.hs:22:15: error:
-    • Couldn't match expected type ‘forall a. a -> a
-                  with actual type ‘Char -> Char
+    • Couldn't match expected type ‘Char -> Char
+                  with actual type ‘forall a. a -> a
     • When checking that the pattern signature: forall a. a -> a
         fits the type of its context: Char -> Char
       In the pattern: x :: forall a. a -> a
index f75f77c..8521731 100644 (file)
@@ -16,7 +16,7 @@ tcfail140.hs:12:10: error:
       In the expression: 3 `f` 4
       In an equation for ‘rot’: rot xs = 3 `f` 4
     • Relevant bindings include
-        rot :: t1 -> t (bound at tcfail140.hs:12:1)
+        rot :: p -> t (bound at tcfail140.hs:12:1)
 
 tcfail140.hs:14:15: error:
     • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
@@ -36,6 +36,6 @@ tcfail140.hs:16:8: error:
       In the expression: (\ Just x -> x) :: Maybe a -> a
 
 tcfail140.hs:19:1: error:
-    • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’
+    • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’
     • The equation(s) for ‘g’ have two arguments,
       but its type ‘Int -> Int’ has only one
index a231133..30e27b8 100644 (file)
@@ -3,7 +3,7 @@ tcfail181.hs:17:9: error:
     • Could not deduce (Monad m0) arising from a use of ‘foo’
       from the context: Monad m
         bound by the inferred type of
-                 wog :: Monad m => t -> Something (m Bool) e
+                 wog :: Monad m => p -> Something (m Bool) e
         at tcfail181.hs:17:1-30
       The type variable ‘m0’ is ambiguous
       These potential instances exist:
index ded8833..db43554 100644 (file)
@@ -1,4 +1,4 @@
 
 T12574.hs:3:1: warning: [-Wmissing-local-signatures]
     Polymorphic local binding with no type signature:
-      T12574.id :: forall t. t -> t
+      T12574.id :: forall p. p -> p