Orient TyVar/TyVar equalities with deepest on the left
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 18 May 2018 07:43:11 +0000 (08:43 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 18 May 2018 16:16:17 +0000 (17:16 +0100)
Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable).  Either way, deepest wins:
see TcUnify Note [Deeper level on the left].

This observation led me to some significant changes:

* A SkolemTv already had a TcLevel, but the level wasn't really being
  used.   Now it is!

* I updated added invariant (SkolInf) to TcType
  Note [TcLevel and untouchable type variables], documenting that
  the level number of all the ic_skols should be the same as the
  ic_tclvl of the implication

* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
  zero, which messed the scheme up.   Now they get a level number the
  same way as all other TcTyVars, instead of being a special case.

* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
  was previously done via their magic zero level) isTouchableMetaTyVar
  just tests for those two cases.

* TcUnify.swapOverTyVars is the crucial orientation function; see the
  new Note [TyVar/TyVar orientation].  I completely rewrote this function,
  and it's now much much easier to understand.

I ended up doing some related refactoring, of course

* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
  a lot of useless work in the case where there are no skolems; I
  added a fast-patch

* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
  the higher-order parameter to tcExpliciTKBndrsX.

* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
  by analogy with TcUnify.checkConstraints.

* Inline TcUnify.buildImplication into its only call-site in
  TcUnify.checkConstraints

* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
  simpler API

* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
  nuke the latter, adding Note [No evidence bindings] to TcEvidence.

39 files changed:
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/ado/T13242a.stderr
testsuite/tests/dependent/should_fail/T14066d.stderr
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/gadt/T15009.hs [new file with mode: 0644]
testsuite/tests/gadt/all.T
testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
testsuite/tests/indexed-types/should_fail/T13784.stderr
testsuite/tests/partial-sigs/should_fail/T14040a.stderr
testsuite/tests/polykinds/T13555.stderr
testsuite/tests/polykinds/T14846.hs
testsuite/tests/polykinds/T14846.stderr
testsuite/tests/polykinds/T7230.stderr
testsuite/tests/polykinds/T8566.stderr
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/typecheck/should_compile/ExPatFail.stderr
testsuite/tests/typecheck/should_compile/T9834.stderr
testsuite/tests/typecheck/should_compile/tc141.stderr
testsuite/tests/typecheck/should_fail/T14607.hs
testsuite/tests/typecheck/should_fail/T14607.stderr
testsuite/tests/typecheck/should_fail/T7453.stderr
testsuite/tests/typecheck/should_fail/T7869.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail068.stderr
testsuite/tests/typecheck/should_fail/tcfail076.stderr
testsuite/tests/typecheck/should_fail/tcfail099.stderr
testsuite/tests/typecheck/should_fail/tcfail103.stderr
testsuite/tests/typecheck/should_fail/tcfail174.stderr
testsuite/tests/typecheck/should_fail/tcfail198.stderr

index dc85fe2..dfebb87 100644 (file)
@@ -747,14 +747,9 @@ can_eq_nc_forall ev eq_rel s1 s2
 
             empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
 
-      ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
-                                       go skol_tvs empty_subst2 bndrs2
-           -- We have nowhere to put these bindings
-           -- but TcSimplify.setImplicationStatus
-           -- checks that we don't actually use them
-           -- when skol_info = UnifyForAllSkol
-
-      ; updWorkListTcS (extendWorkListImplic implic)
+      ; all_co <- checkConstraintsTcS skol_info skol_tvs $
+                  go skol_tvs empty_subst2 bndrs2
+
       ; setWantedEq orig_dest all_co
       ; stopWith ev "Deferred polytype equality" } }
 
@@ -1757,24 +1752,6 @@ canEqTyVarTyVar, are these
    substituted out  Note [Elminate flat-skols]
         fsk ~ a
 
-Note [Eliminate flat-skols]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have  [G] Num (F [a])
-then we flatten to
-     [G] Num fsk
-     [G] F [a] ~ fsk
-where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
-      type instance F [a] = a
-then we'll reduce the second constraint to
-     [G] a ~ fsk
-and then replace all uses of 'a' with fsk.  That's bad because
-in error messages intead of saying 'a' we'll say (F [a]).  In all
-places, including those where the programmer wrote 'a' in the first
-place.  Very confusing!  See Trac #7862.
-
-Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
-the fsk.
-
 Note [Equalities with incompatible kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 What do we do when we have an equality
index 7a681b5..1172c0a 100644 (file)
@@ -413,10 +413,9 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
                      , ic_given = map (tidyEvVar env1) given
                      , ic_info  = info' }
     ctxt1 | NoEvBindsVar{} <- evb    = noDeferredBindings ctxt
-          | termEvidenceAllowed info = ctxt
-          | otherwise                = noDeferredBindings ctxt
+          | otherwise                = ctxt
           -- If we go inside an implication that has no term
-          -- evidence (i.e. unifying under a forall), we can't defer
+          -- evidence (e.g. unifying under a forall), we can't defer
           -- type errors.  You could imagine using the /enclosing/
           -- bindings (in cec_binds), but that may not have enough stuff
           -- in scope for the bindings to be well typed.  So we just
index 1065a15..2aa2f16 100644 (file)
@@ -401,10 +401,9 @@ data EvBindsVar
       -- See Note [Tracking redundant constraints] in TcSimplify
     }
 
-  | NoEvBindsVar {  -- used when we're solving only for equalities,
-                    -- which don't have bindings
+  | NoEvBindsVar {  -- See Note [No evidence bindings]
 
-        -- see above for comments
+      -- See above for comments on ebv_uniq, evb_tcvs
       ebv_uniq :: Unique,
       ebv_tcvs :: IORef CoVarSet
     }
@@ -415,6 +414,21 @@ instance Data.Data TcEvBinds where
   gunfold _ _  = error "gunfold"
   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
 
+{- Note [No evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Class constraints etc give rise to /term/ bindings for evidence, and
+we have nowhere to put term bindings in /types/.  So in some places we
+use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level
+evidence bindings are allowed.  Notebly ():
+
+  - Places in types where we are solving kind constraints (all of which
+    are equalities); see solveEqualities, solveLocalEqualities,
+    checkTvConstraints
+
+  - When unifying forall-types
+-}
+
 -----------------
 newtype EvBindMap
   = EvBindMap {
index 3bee41f..125891f 100644 (file)
@@ -18,8 +18,8 @@ module TcHsType (
         tcHsDeriv, tcHsVectInst,
         tcHsTypeApp,
         UserTypeCtxt(..),
-        tcImplicitTKBndrs, tcImplicitTKBndrsX, tcImplicitTKBndrsSig,
-        tcExplicitTKBndrs, tcExplicitTKBndrsX, tcExplicitTKBndrsSig,
+        tcImplicitTKBndrs, tcImplicitTKBndrsX,
+        tcExplicitTKBndrs,
         kcExplicitTKBndrs, kcImplicitTKBndrs,
 
                 -- Type checking type and class decls
@@ -247,11 +247,12 @@ tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
          --    kind variables floating about, immediately prior to
          --    kind generalisation
 
-         -- We use "InKnot", because this is called on class method sigs
-         -- in the knot
+         -- We use the "InKnot" zonker, because this is called
+         -- on class method sigs in the knot
        ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
        ; kvs <- kindGeneralize ty1
        ; zonkSigType (mkInvForAllTys kvs ty1) }
+
 tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
 
 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
@@ -267,6 +268,7 @@ tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
           -- need to promote any remaining metavariables; test case:
           -- dependent/should_fail/T14066e.
        ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
+
 tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
 
 -----------------
@@ -395,7 +397,7 @@ Answer: we use the same rule as for value bindings:
  * Additionally, we attempt to generalise if we have NoMonoLocalBinds
 
 Trac #13337 shows the problem if we kind-generalise an open type (i.e.
-one that mentions in-scope tpe variable
+one that mentions in-scope type variable
   foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
       => proxy a -> String
   foo _ = case eqT :: Maybe (k :~: Type) of
@@ -407,7 +409,7 @@ but (Int :: Type).  Since (:~:) is kind-homogeneous, this requires
 k ~ *, which is true in the Refl branch of the outer case.
 
 That equality will be solved if we allow it to float out to the
-implication constraint for the Refl match, bnot not if we aggressively
+implication constraint for the Refl match, but not not if we aggressively
 attempt to solve all equalities the moment they occur; that is, when
 checking (Maybe (a :~: Int)).   (NB: solveEqualities fails unless it
 solves all the kind equalities, which is the right thing at top level.)
@@ -1766,24 +1768,31 @@ tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
                    -> [Name]
                    -> TcM a
                    -> TcM ([TcTyVar], a)   -- these tyvars are dependency-ordered
--- Returned TcTyVars have the supplied HsTyVarBndrs,
--- but may be in different order to the original [Name]
+-- * Guarantees to call solveLocalEqualities to unify
+--   all constraints from thing_inside.
+--
+-- * Returned TcTyVars have the supplied HsTyVarBndrs,
+--   but may be in different order to the original [Name]
 --   (because of sorting to respect dependency)
--- Returned TcTyVars have zonked kinds
--- See Note [Keeping scoped variables in order: Implicit]
+--
+-- * Returned TcTyVars have zonked kinds
+--   See Note [Keeping scoped variables in order: Implicit]
 tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
+  | null tv_names -- Short cut for the common case where there
+                  -- are no implicit type variables to bind
+  = do { result <- solveLocalEqualities thing_inside
+       ; return ([], result) }
+
+  | otherwise
   = do { (skol_tvs, result)
            <- solveLocalEqualities $
-              do { (inner_tclvl, wanted, (skol_tvs, result))
-                     <- pushLevelAndCaptureConstraints $
-                     do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
-                        ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
-                        ; result <- tcExtendTyVarEnv must_scope_tvs $
-                                    thing_inside
-                        ; return (map fst tv_pairs, result) }
+              checkTvConstraints skol_info Nothing $
+              do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
+                 ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
+                 ; result <- tcExtendTyVarEnv must_scope_tvs $
+                             thing_inside
+                 ; return (map fst tv_pairs, result) }
 
-                 ; emitTvImplication inner_tclvl skol_tvs Nothing wanted skol_info
-                 ; return (skol_tvs, result) }
 
        ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
           -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
@@ -1812,24 +1821,8 @@ tcExplicitTKBndrs :: SkolemInfo
                   -> [LHsTyVarBndr GhcRn]
                   -> TcM a
                   -> TcM ([TcTyVar], a)
--- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
-tcExplicitTKBndrs = tcExplicitTKBndrsX newSkolemTyVar
-
--- | This brings a bunch of tyvars into scope as SigTvs, where they can unify
--- with other type *variables* only.
-tcExplicitTKBndrsSig :: SkolemInfo
-                     -> [LHsTyVarBndr GhcRn]
-                     -> TcM a
-                     -> TcM ([TcTyVar], a)
-tcExplicitTKBndrsSig = tcExplicitTKBndrsX newSigTyVar
-
-tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar)
-                   -> SkolemInfo
-                   -> [LHsTyVarBndr GhcRn]
-                   -> TcM a
-                   -> TcM ([TcTyVar], a)
 -- See also Note [Associated type tyvar names] in Class
-tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
+tcExplicitTKBndrs skol_info hs_tvs thing_inside
 -- This function brings into scope a telescope of binders as written by
 -- the user. At first blush, it would then seem that we should bring
 -- them into scope one at a time, bumping the TcLevel each time.
@@ -1840,11 +1833,16 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
 -- notice that the telescope is out of order. That's what we do here,
 -- following the logic of tcImplicitTKBndrsX.
 -- See also Note [Keeping scoped variables in order: Explicit]
-  = do { (inner_tclvl, wanted, (skol_tvs, result))
-           <- pushLevelAndCaptureConstraints $
-              bind_tvbs hs_tvs
+--
+-- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
+  | null hs_tvs  -- Short cut that avoids creating an implication
+                 -- constraint in the common case where none is needed
+  = do { result <- thing_inside
+       ; return ([], result) }
 
-       ; emitTvImplication inner_tclvl skol_tvs (Just doc) wanted skol_info
+  | otherwise
+  = do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $
+                               bind_tvbs hs_tvs
 
        ; traceTc "tcExplicitTKBndrs" $
            vcat [ text "Hs vars:" <+> ppr hs_tvs
@@ -1856,7 +1854,7 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
     bind_tvbs [] = do { result <- thing_inside
                       ; return ([], result) }
     bind_tvbs (L _ tvb : tvbs)
-      = do { (tv, in_scope) <- tcHsTyVarBndr new_tv tvb
+      = do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
            ; (if in_scope then id else tcExtendTyVarEnv [tv]) $
            do { (tvs, result) <- bind_tvbs tvbs
               ; return (tv : tvs, result) }}
@@ -1874,28 +1872,6 @@ kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
        ; tcExtendTyVarEnv [tv] $
          kcExplicitTKBndrs hs_tvs thing_inside }
 
--- | Build and emit an Implication appropriate for type-checking a type.
--- This assumes all constraints will be equality constraints, and
--- so does not create an EvBindsVar
-emitTvImplication :: TcLevel    -- of the constraints
-                   -> [TcTyVar]  -- skolems
-                   -> Maybe SDoc  -- user-written telescope, if present
-                   -> WantedConstraints
-                   -> SkolemInfo
-                   -> TcM ()
-emitTvImplication inner_tclvl skol_tvs m_telescope wanted skol_info
-  = do { tc_lcl_env <- getLclEnv
-       ; ev_binds   <- newNoTcEvBinds
-       ; let implic = newImplication { ic_tclvl  = inner_tclvl
-                                     , ic_skols  = skol_tvs
-                                     , ic_telescope = m_telescope
-                                     , ic_no_eqs = True
-                                     , ic_wanted = wanted
-                                     , ic_binds  = ev_binds
-                                     , ic_info   = skol_info
-                                     , ic_env    = tc_lcl_env }
-       ; emitImplication implic }
-
 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
               -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
 -- Return a TcTyVar, built using the provided function
index b1bc1d0..398d345 100644 (file)
@@ -512,13 +512,24 @@ tcInstSkolTyVars' overlappable subst tvs
        ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
 
 mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
-mkTcSkolTyVar lvl loc overlappable old_name kind
+-- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
+-- See Note [Skolem level allocation]
+mkTcSkolTyVar tc_lvl loc overlappable old_name kind
   = do { uniq <- newUnique
        ; let name = mkInternalName uniq (getOccName old_name) loc
        ; return (mkTcTyVar name kind details) }
   where
-    details = SkolemTv (pushTcLevel lvl) overlappable
-              -- NB: skolems bump the level
+    details = SkolemTv (pushTcLevel tc_lvl) overlappable
+              -- pushTcLevel: see Note [Skolem level allocation]
+
+{- Note [Skolem level allocation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
+So we want their level to the level of the soon-to-be-created implication,
+which has a level one higher than the current level.  Hence the pushTcLevel.
+It feels like a slight hack.  Applies also to vanillaSkolemTv.
+
+-}
 
 ------------------
 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
@@ -569,9 +580,10 @@ newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
   = do { uniq <- newUnique
        ; ref  <- newMutVar Flexi
+       ; tclvl <- getTcLevel
        ; let details = MetaTv { mtv_info  = FlatSkolTv
                               , mtv_ref   = ref
-                              , mtv_tclvl = fmvTcLevel }
+                              , mtv_tclvl = tclvl }
              name = mkMetaTyVarName uniq (fsLit "fsk")
        ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
@@ -624,9 +636,10 @@ newFmvTyVar :: TcType -> TcM TcTyVar
 newFmvTyVar fam_ty
   = do { uniq <- newUnique
        ; ref  <- newMutVar Flexi
+       ; tclvl <- getTcLevel
        ; let details = MetaTv { mtv_info  = FlatMetaTv
                               , mtv_ref   = ref
-                              , mtv_tclvl = fmvTcLevel }
+                              , mtv_tclvl = tclvl }
              name = mkMetaTyVarName uniq (fsLit "s")
        ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
index d3f5c68..f39ce52 100644 (file)
@@ -636,9 +636,9 @@ 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 vanillaSkolemTv
+       ; let rr_tv  = mkTyVar rr_name runtimeRepTy
              rr     = mkTyVarTy rr_tv
-             res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
+             res_tv = mkTyVar tv_name (tYPE rr)
              res_ty = mkTyVarTy res_tv
              is_unlifted = null args && null prov_dicts
              (cont_args, cont_arg_tys)
@@ -686,7 +686,7 @@ tcPatSynMatcher (L loc name) lpat
                        }
              match = mkMatch (mkPrefixFunRhs (L loc name)) []
                              (mkHsLams (rr_tv:res_tv:univ_tvs)
-                             req_dicts body')
+                                       req_dicts body')
                              (noLoc (EmptyLocalBinds noExt))
              mg :: MatchGroup GhcTc (LHsExpr GhcTc)
              mg = MG{ mg_alts = L (getLoc match) [match]
index 968330d..cc5c7ec 100644 (file)
@@ -106,7 +106,6 @@ module TcRnTypes(
 
 
         SkolemInfo(..), pprSigSkolInfo, pprSkolInfo,
-        termEvidenceAllowed,
 
         CtEvidence(..), TcEvDest(..),
         mkKindLoc, toKindLoc, mkGivenLoc,
@@ -3228,14 +3227,6 @@ 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 cx ty _) = pprSigSkolInfo cx ty
index b1da40c..150f9be 100644 (file)
@@ -16,7 +16,7 @@ module TcSMonad (
     TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
     failTcS, warnTcS, addErrTcS,
     runTcSEqualities,
-    nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication,
+    nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS,
 
     runTcPluginTcS, addUsedGRE, addUsedGREs,
 
@@ -1950,8 +1950,12 @@ getNoGivenEqs tclvl skol_tvs
                       -- outer context but were refined to an insoluble by
                       -- a local equality; so do /not/ add ct_given_here.
 
-       ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
-                                        , ppr insols])
+       ; traceTcS "getNoGivenEqs" $
+         vcat [ if has_given_eqs then text "May have given equalities"
+                                 else text "No given equalities"
+              , text "Skols:" <+> ppr skol_tvs
+              , text "Inerts:" <+> ppr inerts
+              , text "Insols:" <+> ppr insols]
        ; return (not has_given_eqs, insols) }
   where
     eqs_given_here :: EqualCtList -> Bool
@@ -2094,6 +2098,10 @@ b) 'a' will have been completely substituted out in the inert set,
    returned as part of 'fsks'
 
 For an example, see Trac #9211.
+
+See also TcUnify Note [Deeper level on the left] for how we ensure
+that the right variable is on the left of the equality when both are
+tyvars.
 -}
 
 removeInertCts :: [Ct] -> InertCans -> InertCans
@@ -2704,40 +2712,40 @@ nestTcS (TcS thing_inside)
 
        ; return res }
 
-buildImplication :: SkolemInfo
-                 -> [TcTyVar]        -- Skolems
-                 -> [EvVar]          -- Givens
-                 -> TcS result
-                 -> TcS (Bag Implication, TcEvBinds, result)
--- Just like TcUnify.buildImplication, but in the TcS monnad,
+checkConstraintsTcS :: SkolemInfo
+                    -> [TcTyVar]        -- Skolems
+                    -> TcS result
+                    -> TcS result
+-- Just like TcUnify.checkTvConstraints, but in the TcS monnad,
 -- using the work-list to gather the constraints
-buildImplication skol_info skol_tvs givens (TcS thing_inside)
-  = TcS $ \ env ->
+checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
+  = TcS $ \ tcs_env ->
     do { new_wl_var <- TcM.newTcRef emptyWorkList
-       ; tc_lvl <- TcM.getTcLevel
-       ; let new_tclvl = pushTcLevel tc_lvl
+       ; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var }
 
-       ; res <- TcM.setTcLevel new_tclvl $
-                thing_inside (env { tcs_worklist = new_wl_var })
+       ; (res, new_tclvl) <- TcM.pushTcLevelM $
+                             thing_inside new_tcs_env
 
        ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
-       ; if null eqs
-         then return (emptyBag, emptyTcEvBinds, res)
-         else
-    do { env <- TcM.getLclEnv
-       ; ev_binds_var <- TcM.newTcEvBinds
-       ; let wc  = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
-                            null (wl_implics wl), ppr wl )
-                   WC { wc_simple = listToCts eqs
-                      , wc_impl   = emptyBag }
-             imp = newImplication { ic_tclvl  = new_tclvl
-                                  , ic_skols  = skol_tvs
-                                  , ic_given  = givens
-                                  , ic_wanted = wc
-                                  , ic_binds  = ev_binds_var
-                                  , ic_env    = env
-                                  , ic_info   = skol_info }
-      ; return (unitBag imp, TcEvBinds ev_binds_var, res) } }
+       ; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
+                  null (wl_implics wl), ppr wl )
+         unless (null eqs) $
+         do { tcl_env <- TcM.getLclEnv
+            ; ev_binds_var <- TcM.newNoTcEvBinds
+            ; let wc  = WC { wc_simple = listToCts eqs
+                           , wc_impl   = emptyBag }
+                  imp = newImplication { ic_tclvl  = new_tclvl
+                                       , ic_skols  = skol_tvs
+                                       , ic_wanted = wc
+                                       , ic_binds  = ev_binds_var
+                                       , ic_env    = tcl_env
+                                       , ic_info   = skol_info }
+
+           -- Add the implication to the work-list
+           ; TcM.updTcRef (tcs_worklist tcs_env)
+                          (extendWorkListImplic (unitBag imp)) }
+
+      ; return res }
 
 {-
 Note [Propagate the solved dictionaries]
@@ -2778,9 +2786,7 @@ getWorkListImplics
 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
 updWorkListTcS f
   = do { wl_var <- getTcSWorkListRef
-       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
-       ; let new_work = f wl_curr
-       ; wrapTcS (TcM.writeTcRef wl_var new_work) }
+       ; wrapTcS (TcM.updTcRef wl_var f)}
 
 emitWorkNC :: [CtEvidence] -> TcS ()
 emitWorkNC evs
index ccb7ef5..136e60a 100644 (file)
@@ -1725,19 +1725,13 @@ neededEvVars :: Implication -> TcS Implication
 --   - From the 'needed' set, delete ev_bndrs, the binders of the
 --     evidence bindings, to give the final needed variables
 --
-neededEvVars implic@(Implic { ic_info = info
-                            , ic_given = givens
+neededEvVars implic@(Implic { ic_given = givens
                             , ic_binds = ev_binds_var
                             , ic_wanted = WC { wc_impl = implics }
                             , ic_need_inner = old_needs })
  = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
       ; tcvs     <- TcS.getTcEvTyCoVars ev_binds_var
 
-        -- Check that there are no term-level evidence bindings
-        -- in the cases where we have no place to put them
-      ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap ev_binds
-                , ppr info $$ ppr ev_binds )
-
       ; let seeds1        = foldrBag add_implic_seeds old_needs implics
             seeds2        = foldEvBindMap add_wanted seeds1 ev_binds
             seeds3        = seeds2 `unionVarSet` tcvs
index 8295c57..9abd264 100644 (file)
@@ -30,7 +30,7 @@ module TcType (
 
   -- TcLevel
   TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
-  strictlyDeeperThan, sameDepthAs, fmvTcLevel,
+  strictlyDeeperThan, sameDepthAs,
   tcTypeLevel, tcTyVarLevel, maxTcLevel,
   promoteSkolem, promoteSkolemX, promoteSkolemsX,
   --------------------------------
@@ -44,7 +44,7 @@ module TcType (
   isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
-  isTouchableMetaTyVar, isTouchableOrFmv,
+  isTouchableMetaTyVar,
   isFloatedTouchableMetaTyVar,
   findDupSigTvs, mkTyVarNamePairs,
 
@@ -282,8 +282,6 @@ However, the type checker and constraint solver can encounter type
 variables that use the 'TyVar' variant of Var.Var, for a couple of
 reasons:
 
-  - When unifying or flattening under (forall a. ty)
-
   - When typechecking a class decl, say
        class C (a :: k) where
           foo :: T a -> Int
@@ -295,7 +293,10 @@ reasons:
 
     See calls to tcExtendTyVarEnv for other places that ordinary
     TyVars are bought into scope, and hence may show up in the types
-    and inds generated by TcHsType.
+    and kinds generated by TcHsType.
+
+  - The pattern-match overlap checker calls the constraint solver,
+    long afer TcTyVars have been zonked away
 
 It's convenient to simply treat these TyVars as skolem constants,
 which of course they are.  So
@@ -503,6 +504,8 @@ we would need to enforce the separation.
 data TcTyVarDetails
   = SkolemTv      -- A skolem
        TcLevel    -- Level of the implication that binds it
+                  -- See TcUnify Note [Deeper level on the left] for
+                  --     how this level number is used
        Bool       -- True <=> this skolem type variable can be overlapped
                   --          when looking up instances
                   -- See Note [Binding when looking up instances] in InstEnv
@@ -516,8 +519,10 @@ data TcTyVarDetails
 
 vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
 -- See Note [Binding when looking up instances] in InstEnv
-vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False  -- Might be instantiated
-superSkolemTv   = SkolemTv (pushTcLevel topTcLevel) True   -- Treat this as a completely distinct type
+vanillaSkolemTv = SkolemTv topTcLevel False  -- Might be instantiated
+superSkolemTv   = SkolemTv topTcLevel True   -- Treat this as a completely distinct type
+                  -- The choice of level number here is a bit dodgy, but
+                  -- topTcLevel works in the places that vanillaSkolemTv is used
 
 -----------------------------
 data MetaDetails
@@ -689,9 +694,13 @@ Note [TcLevel and untouchable type variables]
     (ImplicInv) The level number (ic_tclvl) of an Implication is
                 STRICTLY GREATER THAN that of its parent
 
-    (GivenInv) The level number of a unification variable appearing
-                 in the 'ic_given' of an implication I should be
-                 STRICTLY LESS THAN the ic_tclvl of I
+    (SkolInv)   The level number of the skolems (ic_skols) of an
+                Implication is equal to the level of the implication
+                itself (ic_tclvl)
+
+    (GivenInv)  The level number of a unification variable appearing
+                in the 'ic_given' of an implication I should be
+                STRICTLY LESS THAN the ic_tclvl of I
 
     (WantedInv) The level number of a unification variable appearing
                 in the 'ic_wanted' of an implication I should be
@@ -699,7 +708,8 @@ Note [TcLevel and untouchable type variables]
                 See Note [WantedInv]
 
 * A unification variable is *touchable* if its level number
-  is EQUAL TO that of its immediate parent implication.
+  is EQUAL TO that of its immediate parent implication,
+  and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv
 
 Note [WantedInv]
 ~~~~~~~~~~~~~~~~
@@ -749,28 +759,21 @@ Note [TcLevel assignment]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 We arrange the TcLevels like this
 
-   0   Level for all flatten meta-vars
-   1   Top level
-   2   First-level implication constraints
-   3   Second-level implication constraints
+   0   Top level
+   1   First-level implication constraints
+   2   Second-level implication constraints
    ...etc...
-
-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
--- See Note [TcLevel assignment]
-fmvTcLevel = TcLevel 0
-
 topTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
-topTcLevel = TcLevel 1   -- 1 = outermost level
+topTcLevel = TcLevel 0   -- 0 = outermost level
 
 isTopTcLevel :: TcLevel -> Bool
-isTopTcLevel (TcLevel 1) = True
+isTopTcLevel (TcLevel 0) = True
 isTopTcLevel _           = False
 
 pushTcLevel :: TcLevel -> TcLevel
@@ -1172,37 +1175,25 @@ tcIsTcTyVar :: TcTyVar -> Bool
 -- See Note [TcTyVars in the typechecker]
 tcIsTcTyVar tv = isTyVar tv
 
-isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
-isTouchableOrFmv ctxt_tclvl tv
-  = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-      MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
-        -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
-                    ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
-           case info of
-             FlatMetaTv -> True
-             _          -> tv_tclvl `sameDepthAs` ctxt_tclvl
-      _          -> False
-
 isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
 isTouchableMetaTyVar ctxt_tclvl tv
   | isTyVar tv -- See Note [Coercion variables in free variable lists]
-  = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-      MetaTv { mtv_tclvl = tv_tclvl }
-        -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
-                    ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
-           tv_tclvl `sameDepthAs` ctxt_tclvl
-      _ -> False
+  , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv
+  , not (isFlattenInfo info)
+  = ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
+             ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
+    tv_tclvl `sameDepthAs` ctxt_tclvl
+
   | otherwise = False
 
 isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
 isFloatedTouchableMetaTyVar ctxt_tclvl tv
   | isTyVar tv -- See Note [Coercion variables in free variable lists]
+  , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv
+  , not (isFlattenInfo info)
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-      MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
-      _ -> False
+    tv_tclvl `strictlyDeeperThan` ctxt_tclvl
+
   | otherwise = False
 
 isImmutableTyVar :: TyVar -> Bool
@@ -1237,7 +1228,10 @@ isFskTyVar tv
 
 -- | True of both given and wanted flatten-skolems (fak and usk)
 isFlattenTyVar tv
-  = isFmvTyVar tv || isFskTyVar tv
+  = ASSERT2( tcIsTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+        MetaTv { mtv_info = info } -> isFlattenInfo info
+        _                          -> False
 
 isSkolemTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
@@ -1284,6 +1278,11 @@ metaTyVarInfo tv
       MetaTv { mtv_info = info } -> info
       _ -> pprPanic "metaTyVarInfo" (ppr tv)
 
+isFlattenInfo :: MetaInfo -> Bool
+isFlattenInfo FlatMetaTv = True
+isFlattenInfo FlatSkolTv = True
+isFlattenInfo _          = False
+
 metaTyVarTcLevel :: TcTyVar -> TcLevel
 metaTyVarTcLevel tv
   = case tcTyVarDetails tv of
index a61b061..4343c32 100644 (file)
@@ -13,7 +13,8 @@ module TcUnify (
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
   tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
   tcSubTypeDS_NC_O, tcSubTypeET,
-  checkConstraints, buildImplicationFor,
+  checkConstraints, checkTvConstraints,
+  buildImplicationFor,
 
   -- Various unifications
   unifyType, unifyTheta, unifyKind,
@@ -1124,29 +1125,45 @@ checkConstraints :: SkolemInfo
                  -> TcM (TcEvBinds, result)
 
 checkConstraints skol_info skol_tvs given thing_inside
-  = do { (implics, ev_binds, result)
-            <- buildImplication skol_info skol_tvs given thing_inside
-       ; emitImplications implics
-       ; return (ev_binds, result) }
-
-buildImplication :: SkolemInfo
-                 -> [TcTyVar]           -- Skolems
-                 -> [EvVar]             -- Given
-                 -> TcM result
-                 -> TcM (Bag Implication, TcEvBinds, result)
-buildImplication skol_info skol_tvs given thing_inside
   = do { implication_needed <- implicationNeeded skol_tvs given
 
        ; if implication_needed
          then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
                  ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
-                 ; return (implics, ev_binds, result) }
+                 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+                 ; emitImplications implics
+                 ; return (ev_binds, result) }
 
          else -- Fast path.  We check every function argument with
               -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
               -- So this fast path is well-exercised
               do { res <- thing_inside
-                 ; return (emptyBag, emptyTcEvBinds, res) } }
+                 ; return (emptyTcEvBinds, res) } }
+
+checkTvConstraints :: SkolemInfo
+                   -> Maybe SDoc  -- User-written telescope, if present
+                   -> TcM ([TcTyVar], result)
+                   -> TcM ([TcTyVar], result)
+
+checkTvConstraints skol_info m_telescope thing_inside
+  = do { (tclvl, wanted, (skol_tvs, result))
+             <- pushLevelAndCaptureConstraints thing_inside
+
+       ; if isEmptyWC wanted
+         then return ()
+         else do { tc_lcl_env <- getLclEnv
+                 ; ev_binds   <- newNoTcEvBinds
+                 ; emitImplication $
+                   newImplication { ic_tclvl     = tclvl
+                                  , ic_skols     = skol_tvs
+                                  , ic_no_eqs    = True
+                                  , ic_telescope = m_telescope
+                                  , ic_wanted    = wanted
+                                  , ic_binds     = ev_binds
+                                  , ic_info      = skol_info
+                                  , ic_env       = tc_lcl_env } }
+       ; return (skol_tvs, result) }
+
 
 implicationNeeded :: [TcTyVar] -> [EvVar] -> TcM Bool
 -- With the solver producing unlifted equalities, we need
@@ -1585,72 +1602,113 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
 swapOverTyVars tv1 tv2
-  | isFmvTyVar tv1 = False  -- See Note [Fmv Orientation Invariant]
-  | isFmvTyVar tv2 = True
-
-  | Just lvl1 <- metaTyVarTcLevel_maybe tv1
-      -- If tv1 is touchable, swap only if tv2 is also
-      -- touchable and it's strictly better to update the latter
-      -- But see Note [Avoid unnecessary swaps]
-  = case metaTyVarTcLevel_maybe tv2 of
-      Nothing   -> False
-      Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
-                | lvl1 `strictlyDeeperThan` lvl2 -> False
-                | otherwise                      -> nicer_to_update_tv2
-
-  -- So tv1 is not a meta tyvar
-  -- If only one is a meta tyvar, put it on the left
-  -- This is not because it'll be solved; but because
-  -- the floating step looks for meta tyvars on the left
-  | isMetaTyVar tv2 = True
-
-  -- So neither is a meta tyvar (including FlatMetaTv)
-
-  -- If only one is a flatten skolem, put it on the left
-  -- See Note [Eliminate flat-skols]
-  | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
+  -- Level comparison: see Note [TyVar/TyVar orientation]
+  | lvl1 `strictlyDeeperThan` lvl2 = False
+  | lvl2 `strictlyDeeperThan` lvl1 = True
+
+  -- Priority: see Note [TyVar/TyVar orientation]
+  | pri1 > pri2 = False
+  | pri2 > pri1 = True
+
+  -- Names: see Note [TyVar/TyVar orientation]
+  | isSystemName tv2_name, not (isSystemName tv1_name) = True
 
   | otherwise = False
 
   where
+    lvl1 = tcTyVarLevel tv1
+    lvl2 = tcTyVarLevel tv2
+    pri1 = lhsPriority tv1
+    pri2 = lhsPriority tv2
     tv1_name = Var.varName tv1
     tv2_name = Var.varName tv2
 
-    nicer_to_update_tv2
-      | isSigTyVar tv1, not (isSigTyVar tv2)               = True
-      | isSystemName tv2_name, not (isSystemName tv1_name) = True
---      | nameUnique tv1_name `ltUnique` nameUnique tv2_name = True
---      -- See Note [Eliminate younger unification variables]
---      (which also explains why it's commented out)
-      | otherwise = False
 
+lhsPriority :: TcTyVar -> Int
+-- Higher => more important to be on the LHS
+-- See Note [TyVar/TyVar orientation]
+lhsPriority tv
+  = ASSERT2( isTyVar tv, ppr tv)
+    case tcTyVarDetails tv of
+      RuntimeUnk  -> 0
+      SkolemTv {} -> 0
+      MetaTv { mtv_info = info } -> case info of
+                                     FlatSkolTv -> 1
+                                     SigTv      -> 2
+                                     TauTv      -> 3
+                                     FlatMetaTv -> 4
+{- Note [TyVar/TyVar orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
+This is a surprisingly tricky question!
 
--- @trySpontaneousSolve wi@ solves equalities where one side is a
--- touchable unification variable.
--- Returns True <=> spontaneous solve happened
-canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
-canSolveByUnification tclvl tv xi
-  | isTouchableMetaTyVar tclvl tv
-  = case metaTyVarInfo tv of
-      SigTv -> is_tyvar xi
-      _     -> True
+First note: only swap if you have to!
+   See Note [Avoid unnecessary swaps]
 
-  | otherwise    -- Untouchable
-  = False
-  where
-    is_tyvar xi
-      = case tcGetTyVar_maybe xi of
-          Nothing -> False
-          Just tv -> case tcTyVarDetails tv of
-                       MetaTv { mtv_info = info }
-                                   -> case info of
-                                        SigTv -> True
-                                        _     -> False
-                       SkolemTv {} -> True
-                       RuntimeUnk  -> True
+So we look for a positive reason to swap, using a three-step test:
 
-{- Note [Fmv Orientation Invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Level comparison. If 'a' has deeper level than 'b',
+  put 'a' on the left.  See Note [Deeper level on the left]
+
+* Priority.  If the levels are the same, look at what kind of
+  type variable it is, using 'lhsPriority'
+
+  - FlatMetaTv: Always put on the left.
+    See Note [Fmv Orientation Invariant]
+    NB: FlatMetaTvs always have the current level, never an
+        outer one.  So nothing can be deeper than a FlatMetaTv
+
+
+  - SigTv/TauTv:  if we have  sig_tv ~ tau_tv, put tau_tv
+                  on the left because there are fewer
+                  restrictions on updating TauTvs
+
+  - SigTv/TauTv:  put on the left eitehr
+     a) Because it's touchable and can be unified, or
+     b) Even if it's not touchable, TcSimplify.floatEqualities
+        looks for meta tyvars on the left
+
+  - FlatSkolTv: Put on the left in preference to a SkolemTv
+                See Note [Eliminate flat-skols]
+
+* Names. If the level and priority comparisons are all
+  equal, try to eliminate a TyVars with a System Name in
+  favour of ones with a Name derived from a user type signature
+
+* Age.  At one point in the past we tried to break any remaining
+  ties by eliminating the younger type variable, based on their
+  Uniques.  See Note [Eliminate younger unification variables]
+  (which also explains why we don't do this any more)
+
+Note [Deeper level on the left]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The most important thing is that we want to put tyvars with
+the deepest level on the left.  The reason to do so differs for
+Wanteds and Givens, but either way, deepest wins!  Simple.
+
+* Wanteds.  Putting the deepest variable on the left maximise the
+  chances that it's a touchable meta-tyvar which can be solved.
+
+* Givens. Suppose we have something like
+     forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
+
+  If we orient the Given a[2] on the left, we'll rewrite the Wanted to
+  (beta[1] ~ b[1]), and that can float out of the implication.
+  Otherwise it can't.  By putting the deepest variable on the left
+  we maximise our changes of elminating skolem capture.
+
+  See also TcSMonad Note [Let-bound skolems] for another reason
+  to orient with the deepest skolem on the left.
+
+  IMPORTANT NOTE: this test does a level-number comparison on
+  skolems, so it's important that skolems have (accurate) level
+  numbers.
+
+See Trac #15009 for an further analysis of why "deepest on the left"
+is a good plan.
+
+Note [Fmv Orientation Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * We always orient a constraint
         fmv ~ alpha
      with fmv on the left, even if alpha is
@@ -1683,12 +1741,30 @@ T10226, T10009.)
           [WD] F fmv ~ fmv, [WD] fmv ~ a
     And now we are stuck.
 
-So instead the Fmv Orientation Invariant puts te fmv on the
+So instead the Fmv Orientation Invariant puts the fmv on the
 left, giving
       [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
 
     Now we get alpha:=a, and everything works out
 
+Note [Eliminate flat-skols]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have  [G] Num (F [a])
+then we flatten to
+     [G] Num fsk
+     [G] F [a] ~ fsk
+where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
+      type instance F [a] = a
+then we'll reduce the second constraint to
+     [G] a ~ fsk
+and then replace all uses of 'a' with fsk.  That's bad because
+in error messages intead of saying 'a' we'll say (F [a]).  In all
+places, including those where the programmer wrote 'a' in the first
+place.  Very confusing!  See Trac #7862.
+
+Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
+the fsk.
+
 Note [Avoid unnecessary swaps]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we swap without actually improving matters, we can get an infinite loop.
@@ -1719,10 +1795,34 @@ But, to my surprise, it didn't seem to make any significant difference
 to the compiler's performance, so I didn't take it any further.  Still
 it seemed to too nice to discard altogether, so I'm leaving these
 notes.  SLPJ Jan 18.
+-}
 
+-- @trySpontaneousSolve wi@ solves equalities where one side is a
+-- touchable unification variable.
+-- Returns True <=> spontaneous solve happened
+canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
+canSolveByUnification tclvl tv xi
+  | isTouchableMetaTyVar tclvl tv
+  = case metaTyVarInfo tv of
+      SigTv -> is_tyvar xi
+      _     -> True
 
-Note [Prevent unification with type families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  | otherwise    -- Untouchable
+  = False
+  where
+    is_tyvar xi
+      = case tcGetTyVar_maybe xi of
+          Nothing -> False
+          Just tv -> case tcTyVarDetails tv of
+                       MetaTv { mtv_info = info }
+                                   -> case info of
+                                        SigTv -> True
+                                        _     -> False
+                       SkolemTv {} -> True
+                       RuntimeUnk  -> True
+
+{- Note [Prevent unification with type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We prevent unification with type families because of an uneasy compromise.
 It's perfectly sound to unify with type families, and it even improves the
 error messages in the testsuite. It also modestly improves performance, at
@@ -1849,7 +1949,7 @@ lookupTcTyVar tyvar
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat an untouchable type variable as if it was a skolem.  That
-ensures it won't unify with anything.  It's a slight had, because
+ensures it won't unify with anything.  It's a slight hack, because
 we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
index c3dbbba..e03f471 100644 (file)
@@ -1,8 +1,7 @@
 
 T13242a.hs:10:5: error:
     • Couldn't match expected type ‘a0’ with actual type ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a’ is a rigid type variable bound by
         a pattern with constructor: A :: forall a. Eq a => a -> T,
         in a pattern binding in
              'do' block
@@ -28,7 +27,7 @@ T13242a.hs:13:11: error:
       These potential instances exist:
         instance Eq Ordering -- Defined in ‘GHC.Classes’
         instance Eq Integer
-          -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’
+          -- Defined in ‘integer-gmp-1.0.2.0:GHC.Integer.Type’
         instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
         ...plus 22 others
         ...plus six instances involving out-of-scope types
index 3a8b90e..3f5eb98 100644 (file)
@@ -1,14 +1,14 @@
 
 T14066d.hs:11:35: error:
-    • Couldn't match type ‘b’ with ‘b1’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall b. b -> (Proxy Maybe, ())
-        at T14066d.hs:10:1-37
+    • Couldn't match type ‘b1’ with ‘b’
       ‘b1’ is a rigid type variable bound by
         a type expected by the context:
           forall c b1 (a :: c). (Proxy a, Proxy c, b1)
         at T14066d.hs:11:33-35
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
       Expected type: (Proxy a, Proxy c, b1)
         Actual type: (Proxy a, Proxy c, b)
     • In the first argument of ‘g’, namely ‘y’
index 63375ae..bdb6ca5 100644 (file)
@@ -108,15 +108,15 @@ Derived type family instances:
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]]
+GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
   GHC.Base.sconcat = GHC.Base.$dmsconcat
-                       @(T14578.App f[ssk:2] a[ssk:2])
+                       @(T14578.App f[ssk:1] a[ssk:1])
 
 
 
 ==================== Filling in method body ====================
-GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]]
+GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]]
   GHC.Base.stimes = GHC.Base.$dmstimes
-                      @(T14578.App f[ssk:2] a[ssk:2])
+                      @(T14578.App f[ssk:1] a[ssk:1])
 
 
diff --git a/testsuite/tests/gadt/T15009.hs b/testsuite/tests/gadt/T15009.hs
new file mode 100644 (file)
index 0000000..58e17af
--- /dev/null
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs #-}
+
+module T15009 where
+
+-- T2 is an ordinary H98 data type,
+-- and f2 should typecheck with no problem
+data T2 a where
+  MkT2 :: a -> T2 a
+
+f2 (MkT2 x) = not x
+
+-- T1 is a GADT, but the equality is really just a 'let'
+-- so f1 should also typecheck no problem
+data T1 a where
+  MkT1 :: b ~ a => b -> T1 a
+
+f1 (MkT1 x) = not x
+
+
+
index 4c8eb80..321d67e 100644 (file)
@@ -117,3 +117,4 @@ test('T12468', normal, compile_fail, [''])
 test('T14320', normal, compile, [''])
 test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14808', normal, compile, [''])
+test('T15009', normal, compile, [''])
index fa19be4..5b6863c 100644 (file)
@@ -1,11 +1,17 @@
 
 PushedInAsGivens.hs:10:31: error:
-    • Couldn't match expected type ‘a1’ with actual type ‘a’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Could not deduce: a1 ~ a
+      from the context: F Int ~ [a1]
+        bound by the type signature for:
+                   foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
+        at PushedInAsGivens.hs:9:13-44
+      ‘a1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
         at PushedInAsGivens.hs:9:13-44
+      ‘a’ is a rigid type variable bound by
+        the inferred type of bar :: a -> (a, Int)
+        at PushedInAsGivens.hs:(9,1)-(11,20)
     • In the expression: y
       In the first argument of ‘length’, namely ‘[x, y]’
       In the expression: length [x, y]
index 79007ba..ee4ec20 100644 (file)
@@ -1,44 +1,38 @@
 
 T13784.hs:28:28: error:
-    • Could not deduce: as1 ~ (a1 : Divide a1 as1)
-      from the context: (a : as) ~ (a1 : as1)
-        bound by a pattern with constructor:
-                   :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
-                 in an equation for ‘divide’
-        at T13784.hs:28:13-19
-      ‘as1’ is a rigid type variable bound by
-        a pattern with constructor:
-          :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
-        in an equation for ‘divide’
-        at T13784.hs:28:13-19
+    • Couldn't match type ‘as’ with ‘a : Divide a as’
+      ‘as’ is a rigid type variable bound by
+        the instance declaration
+        at T13784.hs:24:10-30
       Expected type: Product (Divide a (a : as))
         Actual type: Product as1
     • In the expression: as
       In the expression: (a, as)
       In an equation for ‘divide’: divide (a :* as) = (a, as)
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:28:18)
-        a :: a1 (bound at T13784.hs:28:13)
+        divide :: Product (a : as) -> (a, Product (Divide a (a : as)))
+          (bound at T13784.hs:28:5)
 
 T13784.hs:32:24: error:
-    • Couldn't match type ‘Product (a1 : as0)’
-                     with ‘(b, Product (Divide b (a1 : as1)))’
+    • Couldn't match type ‘Product (a : as0)’
+                     with ‘(b, Product (Divide b (a : as)))’
       Expected type: (b, Product (Divide b (a : as)))
         Actual type: Product (a1 : as0)
     • In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
       In the instance declaration for ‘Divideable b (a : as)’
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:32:18)
-        a :: a1 (bound at T13784.hs:32:13)
         divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
           (bound at T13784.hs:32:5)
 
 T13784.hs:32:29: error:
-    • Couldn't match expected type ‘Product as0’
-                  with actual type ‘(a0, Product (Divide a0 as1))’
+    • Couldn't match type ‘(a0, Product (Divide a0 as))’
+                     with ‘Product as0’
+      Expected type: Product as0
+        Actual type: (a0, Product (Divide a0 as1))
     • In the second argument of ‘(:*)’, namely ‘divide as’
       In the expression: a :* divide as
       In an equation for ‘divide’: divide (a :* as) = a :* divide as
     • Relevant bindings include
-        as :: Product as1 (bound at T13784.hs:32:18)
+        divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
+          (bound at T13784.hs:32:5)
index cc0d0ca..c0e0664 100644 (file)
@@ -1,27 +1,29 @@
 
 T14040a.hs:21:18: error:
-    • Couldn't match type ‘k0’ with ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘a’ with ‘k0’
+      ‘a’ is a rigid type variable bound by
         the type signature for:
           elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
                                                                 x -> WeirdList x -> *).
                            Sing wl
                            -> (forall y. p k0 w0 'WeirdNil)
                            -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                               Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                           -> p k3 w3 wl
+                               Sing x
+                               -> Sing xs -> p (WeirdList k1) w1 xs -> p k1 w2 ('WeirdCons x xs))
+                           -> p k2 w3 wl
         at T14040a.hs:(21,18)-(28,23)
       Expected type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                     -> p k3 w3 wl
+                         Sing x
+                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
+                     -> p k2 w3 wl
         Actual type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                     -> p k3 w3 wl
+                         Sing x
+                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
+                     -> p k2 w3 wl
     • In the ambiguity check for ‘elimWeirdList’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
@@ -39,8 +41,10 @@ T14040a.hs:34:8: error:
                                        -> (forall y. p k0 w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
                                            Sing x
-                                           -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-                                       -> p k3 w3 wl’
+                                           -> Sing xs
+                                           -> p (WeirdList k1) w1 xs
+                                           -> p k1 w2 ('WeirdCons x xs))
+                                       -> p k2 w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
index e822f6e..3d2492e 100644 (file)
@@ -1,8 +1,7 @@
 
 T13555.hs:25:14: error:
-    • Couldn't match type ‘k0’ with ‘k2’
-        because type variable ‘k2’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘k2’ with ‘k0’
+      ‘k2’ is a rigid type variable bound by
         the type signature for:
           crtInfo :: forall k2 (m :: k2).
                      Reflects m Int =>
index ad17841..7b96e94 100644 (file)
@@ -34,6 +34,6 @@ data Hom :: Cat k -> Cat (Struct cls) where
 class Category (cat::Cat ob) where
   i :: StructI xx a => ríki a a
 
-instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
-  i :: forall xx a. StructI xx a => Hom ríki a a
+instance Category riki => Category (Hom riki :: Cat (Struct cls)) where
+  i :: forall xx a. StructI xx a => Hom riki a a
   i = case struct :: AStruct (Structured a cls) of
index 828ddf6..1bfa942 100644 (file)
@@ -1,24 +1,24 @@
 
 T14846.hs:38:8: error:
-    • Couldn't match type ‘ríki1’ with ‘Hom ríki’
-      ‘ríki1’ is a rigid type variable bound by
+    • Couldn't match type ‘ríki’ with ‘Hom riki’
+      ‘ríki’ is a rigid type variable bound by
         the type signature for:
           i :: forall k5 (cls1 :: k5
-                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki1 :: Struct
-                                                                                              cls1
-                                                                                            -> Struct
-                                                                                                 cls1
-                                                                                            -> *).
+                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki :: Struct
+                                                                                             cls1
+                                                                                           -> Struct
+                                                                                                cls1
+                                                                                           -> *).
                StructI xx a =>
-               ríki1 a a
+               ríki a a
         at T14846.hs:38:8-48
-      Expected type: ríki1 a a
-        Actual type: Hom ríki a0 a0
+      Expected type: ríki a a
+        Actual type: Hom riki a0 a0
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
         Instance sig: forall (xx :: k0) (a :: Struct cls0).
                       StructI xx a =>
-                      Hom ríki a a
+                      Hom riki a a
            Class sig: forall k1 (cls :: k1
                                         -> Constraint) k2 (xx :: k2) (a :: Struct
                                                                              cls) (ríki :: Struct
@@ -28,32 +28,7 @@ T14846.hs:38:8: error:
                                                                                            -> *).
                       StructI xx a =>
                       ríki a a
-      In the instance declaration for ‘Category (Hom ríki)’
-
-T14846.hs:39:12: error:
-    • Could not deduce (StructI xx1 (Structured a cls))
-        arising from a use of ‘struct’
-      from the context: Category ríki
-        bound by the instance declaration at T14846.hs:37:10-65
-      or from: StructI xx a
-        bound by the type signature for:
-                   i :: forall (xx :: k0) (a :: Struct cls0).
-                        StructI xx a =>
-                        Hom ríki a a
-        at T14846.hs:38:8-48
-      The type variable ‘xx1’ is ambiguous
-      Relevant bindings include
-        i :: Hom ríki a a (bound at T14846.hs:39:3)
-      These potential instance exist:
-        instance forall k (xx :: k) (cls :: k
-                                            -> Constraint) (structured :: Struct cls).
-                 (Structured xx cls ~ structured, cls xx) =>
-                 StructI xx structured
-          -- Defined at T14846.hs:28:10
-    • In the expression: struct :: AStruct (Structured a cls)
-      In the expression: case struct :: AStruct (Structured a cls) of
-      In an equation for ‘i’:
-          i = case struct :: AStruct (Structured a cls) of
+      In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:44: error:
     • Expected kind ‘Struct cls0 -> Constraint’,
@@ -62,4 +37,4 @@ T14846.hs:39:44: error:
       In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
     • Relevant bindings include
-        i :: Hom ríki a a (bound at T14846.hs:39:3)
+        i :: Hom riki a a (bound at T14846.hs:39:3)
index 53b8bcd..48781e8 100644 (file)
@@ -9,13 +9,13 @@ T7230.hs:48:32: error:
         at T7230.hs:47:1-68
       or from: xs ~ (x : xs1)
         bound by a pattern with constructor:
-                   SCons :: forall k (x :: k) (xs :: [k]).
+                   SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:8-27
       or from: xs1 ~ (x1 : xs2)
         bound by a pattern with constructor:
-                   SCons :: forall k (x :: k) (xs :: [k]).
+                   SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:17-26
index 52a4b21..d368d05 100644 (file)
@@ -1,12 +1,12 @@
 
 T8566.hs:32:9: error:
-    • Could not deduce (C ('AA (t1 (I a ps)) as) ps fs0)
+    • Could not deduce (C ('AA (t (I a ps)) as) ps fs0)
         arising from a use of ‘c’
       from the context: C ('AA (t (I a ps)) as) ps fs
         bound by the instance declaration at T8566.hs:30:10-67
       or from: 'AA t (a : as) ~ 'AA t1 as1
         bound by a pattern with constructor:
-                   A :: forall k (t :: k) (as :: [U *]) (r :: [*]). I ('AA t as) r,
+                   A :: forall v (t :: v) (as :: [U *]) (r :: [*]). I ('AA t as) r,
                  in an equation for ‘c’
         at T8566.hs:32:5
       The type variable ‘fs0’ is ambiguous
index a019b9e..604cc1b 100644 (file)
@@ -8,7 +8,7 @@ T9222.hs:13:3: error:
           at T9222.hs:13:3-43
       ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
-          forall k2 k3 (a :: (k2, k3)) (b :: k2) (c :: k3).
+          forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
           ((a ~ '(b, c)) => Proxy b) -> Want a
         at T9222.hs:13:3-43
     • In the ambiguity check for ‘Want’
index 6cc24fc..e38c32b 100644 (file)
@@ -1,12 +1,14 @@
 
 ExPatFail.hs:12:15: error:
     • 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’ is a rigid type variable bound by
         a pattern with constructor:
           MkT :: forall a. Integral a => a -> Int -> T,
         in a pattern binding
         at ExPatFail.hs:12:11-17
+      ‘p’ is a rigid type variable bound by
+        the inferred type of f :: T -> p
+        at ExPatFail.hs:(12,1)-(13,10)
     • In the pattern: MkT y _
       In a pattern binding: MkT y _ = x
       In the expression: let MkT y _ = x in y
index 01b003f..52f207d 100644 (file)
@@ -19,17 +19,17 @@ T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
           (bound at T9834.hs:23:3)
 
 T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘a’ with ‘a1’
+    • Couldn't match type ‘a1’ with ‘a’
+      ‘a1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q)
+        at T9834.hs:23:10-19
       ‘a’ is a rigid type variable bound by
         the type signature for:
           afix :: forall a.
                   (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a)
                   -> p a
         at T9834.hs:22:11-74
-      ‘a1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q)
-        at T9834.hs:23:10-19
       Expected type: Comp p q a1 -> Comp p q a1
         Actual type: Comp p q a -> Comp p q a
     • In the expression: wrapIdComp
index 9c13f17..b2fe9ab 100644 (file)
@@ -8,11 +8,13 @@ tc141.hs:11:12: error:
 
 tc141.hs:11:31: error:
     • Couldn't match expected type ‘a2’ with actual type ‘a’
-        because type variable ‘a2’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a2’ is a rigid type variable bound by
         an expression type signature:
           forall a2. a2
         at tc141.hs:11:34
+      ‘a’ is a rigid type variable bound by
+        the inferred type of f :: (a, a) -> (a1, a)
+        at tc141.hs:11:1-37
     • In the expression: q :: a
       In the expression: (q :: a, p)
       In the expression: let (p :: a, q :: a) = x in (q :: a, p)
@@ -36,11 +38,13 @@ tc141.hs:13:13: error:
 
 tc141.hs:15:18: error:
     • 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
+      ‘a2’ is a rigid type variable bound by
         the type signature for:
           v :: forall a2. a2
         at tc141.hs:14:14-19
+      ‘p’ is a rigid type variable bound by
+        the inferred type of g :: a -> p -> a1
+        at tc141.hs:(13,1)-(16,13)
     • In the expression: b
       In an equation for ‘v’: v = b
       In the expression:
index c05df0b..86c738d 100644 (file)
@@ -25,3 +25,10 @@ instance Mk a where
 -- At some point, this program was accepted. That's fine. But right now,
 -- it's rejected with a kind error, and we can't generally defer kind
 -- errors, so I'm saying that behavior is OK.
+
+-- Later (May 18) the kind error ended up being in an term-level
+-- implication constraint, which /does/ have an evidence binding
+-- So now the kind error can be deferred.
+-- Consequence of a fast-path for tcImplicitTKBndrsX I think.
+
+
index 0a63e53..740f89a 100644 (file)
@@ -1,12 +1,21 @@
 
-T14607.hs:22:9: error:
+T14607.hs:22:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expecting one more argument to ‘LamCons a  '()’
       Expected a type, but ‘LamCons a  '()’ has kind ‘() -> *’
     • In the type signature: mk :: LamCons a  '()
       In the instance declaration for ‘Mk a’
 
-T14607.hs:22:19: error:
+T14607.hs:22:19: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expected a type, but ‘ '()’ has kind ‘()’
     • In the second argument of ‘LamCons’, namely ‘ '()’
       In the type signature: mk :: LamCons a  '()
       In the instance declaration for ‘Mk a’
+
+T14607.hs:23:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘LamCons a '()’
+                  with actual type ‘LamCons a0 a0 '()’
+    • In the expression: mk
+      In an equation for ‘mk’: mk = mk
+      In the instance declaration for ‘Mk a’
+    • Relevant bindings include
+        mk :: LamCons a '() (bound at T14607.hs:23:3)
index 77348c3..d72b6d9 100644 (file)
@@ -1,11 +1,13 @@
 
 T7453.hs:10:30: error:
     • Couldn't match expected type ‘t’ with actual type ‘p’
-        because type variable ‘t’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘t’ is a rigid type variable bound by
         the type signature for:
           z :: forall t. Id t
         at T7453.hs:8:11-19
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast1 :: p -> a
+        at T7453.hs:(7,1)-(10,30)
     • In the first argument of ‘Id’, namely ‘v’
       In the expression: Id v
       In an equation for ‘aux’: aux = Id v
@@ -17,11 +19,13 @@ T7453.hs:10:30: error:
 
 T7453.hs:16:33: error:
     • 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
+      ‘t1’ is a rigid type variable bound by
         the type signature for:
           z :: forall t1. () -> t1
         at T7453.hs:14:11-22
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast2 :: p -> t
+        at T7453.hs:(13,1)-(16,33)
     • In the first argument of ‘const’, namely ‘v’
       In the expression: const v
       In an equation for ‘aux’: aux = const v
@@ -33,11 +37,13 @@ T7453.hs:16:33: error:
 
 T7453.hs:21:15: error:
     • 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
+      ‘t1’ is a rigid type variable bound by
         the type signature for:
           z :: forall t1. t1
         at T7453.hs:20:11-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of cast3 :: p -> t
+        at T7453.hs:(19,1)-(22,33)
     • In the expression: v
       In an equation for ‘z’:
           z = v
index 4cf1cfa..7e01868 100644 (file)
@@ -1,11 +1,13 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘b’ with ‘b1’
-        because type variable ‘b1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘b1’ with ‘b’
+      ‘b1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
+      ‘b’ is a rigid type variable bound by
+        the inferred type of f :: [a] -> b
+        at T7869.hs:3:1-27
       Expected type: [a1] -> b1
         Actual type: [a] -> b
     • In the expression: f x
index 5a3e733..86099ea 100644 (file)
@@ -1,4 +1,4 @@
-
+4607
 test('tcfail001', normal, compile_fail, [''])
 test('tcfail002', normal, compile_fail, [''])
 test('tcfail003', normal, compile_fail, [''])
@@ -467,7 +467,7 @@ test('T14350', normal, compile_fail, [''])
 test('T14390', normal, compile_fail, [''])
 test('MissingExportList03', normal, compile_fail, [''])
 test('T14618', normal, compile_fail, [''])
-test('T14607', normal, compile_fail, [''])
+test('T14607', normal, compile, [''])
 test('T14605', normal, compile_fail, [''])
 test('T14761a', normal, compile_fail, [''])
 test('T14761b', normal, compile_fail, [''])
index bb3f9dd..4318021 100644 (file)
@@ -23,48 +23,48 @@ tcfail068.hs:14:9: error:
           (bound at tcfail068.hs:12:1)
 
 tcfail068.hs:19:9: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (IndTree s a)
+        at tcfail068.hs:(18,9)-(21,19)
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itiap :: forall a s.
                    Constructed a =>
                    (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
         at tcfail068.hs:16:1-75
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:(18,9)-(21,19)
       Expected type: GHC.ST.ST s1 (IndTree s a)
         Actual type: GHC.ST.ST s (IndTree s a)
     • In the first argument of ‘runST’, namely
         ‘(readSTArray arr i
-          >>= \ val -> writeSTArray arr i (f val) >> return arr)’
+            >>= \ val -> writeSTArray arr i (f val) >> return arr)’
       In the expression:
         runST
           (readSTArray arr i
-           >>= \ val -> writeSTArray arr i (f val) >> return arr)
+             >>= \ val -> writeSTArray arr i (f val) >> return arr)
       In an equation for ‘itiap’:
           itiap i f arr
             = runST
                 (readSTArray arr i
-                 >>= \ val -> writeSTArray arr i (f val) >> return arr)
+                   >>= \ val -> writeSTArray arr i (f val) >> return arr)
     • Relevant bindings include
         arr :: IndTree s a (bound at tcfail068.hs:17:11)
         itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
           (bound at tcfail068.hs:17:1)
 
 tcfail068.hs:24:36: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (IndTree s a)
+        at tcfail068.hs:24:29-46
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrap :: forall a s.
                    Constructed a =>
                    ((Int, Int), (Int, Int)) -> (a -> a) -> IndTree s a -> IndTree s a
         at tcfail068.hs:23:1-87
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:24:29-46
       Expected type: GHC.ST.ST s1 (IndTree s a)
         Actual type: GHC.ST.ST s (IndTree s a)
     • In the first argument of ‘runST’, namely ‘(itrap' i k)’
@@ -91,7 +91,11 @@ tcfail068.hs:24:36: error:
           (bound at tcfail068.hs:24:1)
 
 tcfail068.hs:36:46: error:
-    • Couldn't match type ‘s’ with ‘s1’
+    • Couldn't match type ‘s1’ with ‘s’
+      ‘s1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall s1. GHC.ST.ST s1 (c, IndTree s b)
+        at tcfail068.hs:36:40-63
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrapstate :: forall b a c s.
@@ -104,10 +108,6 @@ tcfail068.hs:36:46: error:
                         -> IndTree s b
                         -> (c, IndTree s b)
         at tcfail068.hs:(34,1)-(35,62)
-      ‘s1’ is a rigid type variable bound by
-        a type expected by the context:
-          forall s1. GHC.ST.ST s1 (c, IndTree s b)
-        at tcfail068.hs:36:40-63
       Expected type: GHC.ST.ST s1 (c, IndTree s b)
         Actual type: GHC.ST.ST s (c, IndTree s b)
     • In the first argument of ‘runST’, namely ‘(itrapstate' i k s)’
index 546715a..d4368a4 100644 (file)
@@ -1,14 +1,14 @@
 
 tcfail076.hs:18:82: error:
-    • Couldn't match type ‘res’ with ‘res1’
-      ‘res’ is a rigid type variable bound by
-        a type expected by the context:
-          forall res. (a -> m res) -> m res
-        at tcfail076.hs:18:28-96
+    • Couldn't match type ‘res1’ with ‘res’
       ‘res1’ is a rigid type variable bound by
         a type expected by the context:
           forall res1. (b -> m res1) -> m res1
         at tcfail076.hs:18:64-88
+      ‘res’ is a rigid type variable bound by
+        a type expected by the context:
+          forall res. (a -> m res) -> m res
+        at tcfail076.hs:18:28-96
       Expected type: m res1
         Actual type: m res
     • In the expression: cont a
index bc30866..a04920f 100644 (file)
@@ -1,11 +1,13 @@
 
 tcfail099.hs:9:20: error:
     • 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’ is a rigid type variable bound by
         a pattern with constructor: C :: forall a. (a -> Int) -> DS,
         in an equation for ‘call’
         at tcfail099.hs:9:7-9
+      ‘p’ is a rigid type variable bound by
+        the inferred type of call :: DS -> p -> Int
+        at tcfail099.hs:9:1-22
     • In the first argument of ‘f’, namely ‘arg’
       In the expression: f arg
       In an equation for ‘call’: call (C f) arg = f arg
index ba0694b..2192d8a 100644 (file)
@@ -1,14 +1,14 @@
 
 tcfail103.hs:15:13: error:
-    • Couldn't match type ‘t’ with ‘s’
-      ‘t’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall t. ST t Int
-        at tcfail103.hs:10:1-12
+    • Couldn't match type ‘s’ with ‘t’
       ‘s’ is a rigid type variable bound by
         the type signature for:
           g :: forall s. ST s Int
         at tcfail103.hs:13:9-21
+      ‘t’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall t. ST t Int
+        at tcfail103.hs:10:1-12
       Expected type: ST s Int
         Actual type: ST t Int
     • In the expression: readSTRef v
index e807388..7245351 100644 (file)
@@ -7,11 +7,13 @@ tcfail174.hs:9:5: error:
       In an equation for ‘g’: g = Base id
 
 tcfail174.hs:16:14: error:
-    • Couldn't match type ‘a’ with ‘a1’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match type ‘a1’ with ‘a’
+      ‘a1’ is a rigid type variable bound by
         the type a -> a
         at tcfail174.hs:16:1-14
+      ‘a’ is a rigid type variable bound by
+        the inferred type of h1 :: Capture a
+        at tcfail174.hs:16:1-14
       Expected type: Capture (forall x. x -> a)
         Actual type: Capture (forall a. a -> a)
     • In the first argument of ‘Capture’, namely ‘g’
@@ -23,7 +25,8 @@ tcfail174.hs:16:14: error:
 tcfail174.hs:19:14: error:
     • Couldn't match type ‘a’ with ‘b’
       ‘a’ is a rigid type variable bound by
-        the type a -> a at tcfail174.hs:1:1
+        the type a -> a
+        at tcfail174.hs:1:1
       ‘b’ is a rigid type variable bound by
         the type signature for:
           h2 :: forall b. Capture b
index e8c3852..66c8438 100644 (file)
@@ -1,11 +1,13 @@
 
 tcfail198.hs:6:36: error:
     • Couldn't match expected type ‘a1’ with actual type ‘a’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
           forall a1. a1
         at tcfail198.hs:6:41
+      ‘a’ is a rigid type variable bound by
+        the inferred type of f3 :: [a] -> [a]
+        at tcfail198.hs:6:1-44
     • In the expression: x :: a
       In the second argument of ‘(++)’, namely ‘[x :: a]’
       In the expression: xs ++ [x :: a]