[Git][ghc/ghc][wip/derived-refactor] Actually checkpoint properly.

Richard Eisenberg gitlab at gitlab.haskell.org
Fri Sep 18 21:50:11 UTC 2020



Richard Eisenberg pushed to branch wip/derived-refactor at Glasgow Haskell Compiler / GHC


Commits:
f550eed8 by Richard Eisenberg at 2020-09-18T17:49:50-04:00
Actually checkpoint properly.

- - - - -


19 changed files:

- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Zonk.hs
- compiler/GHC/Types/Id/Make.hs
- testsuite/tests/dependent/should_compile/all.T
- testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
- testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
- testsuite/tests/indexed-types/should_fail/T13972.hs
- testsuite/tests/indexed-types/should_fail/T14230a.stderr
- testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
- testsuite/tests/polykinds/T14172.stderr
- testsuite/tests/th/T11452.stderr


Changes:

=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -556,9 +556,15 @@ instance Outputable ErrorItem where
 
 -- | Makes an error item from a constraint, calculating whether or not
 -- the item should be suppressed. See Note [Wanteds rewrite Wanteds]
--- in GHC.Tc.Types.Constraint
-mkErrorItem :: Ct -> TcM ErrorItem
+-- in GHC.Tc.Types.Constraint. Returns Nothing if we should just ignore
+-- a constraint. See Note [Constraints to ignore].
+mkErrorItem :: Ct -> TcM (Maybe ErrorItem)
 mkErrorItem ct
+  | AssocFamPatOrigin <- ctOrigin ct
+  = do { traceTc "Ignoring constraint:" (ppr ct)
+       ; return Nothing }   -- See Note [Constraints to ignore]
+
+  | otherwise
   = do { let loc = ctLoc ct
              flav = ctFlavour ct
 
@@ -569,11 +575,11 @@ mkErrorItem ct
                    ; return (supp, Just dest) }
            CtDerived {} -> return (False, Nothing)
 
-       ; return $ EI { ei_pred     = ctPred ct
-                     , ei_evdest   = m_evdest
-                     , ei_flavour  = flav
-                     , ei_loc      = loc
-                     , ei_suppress = suppress }}
+       ; return $ Just $ EI { ei_pred     = ctPred ct
+                            , ei_evdest   = m_evdest
+                            , ei_flavour  = flav
+                            , ei_loc      = loc
+                            , ei_suppress = suppress }}
 
 {- "RAE"
 tidyErrorItem :: TidyEnv -> ErrorItem -> ErrorItem
@@ -610,7 +616,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
                                          , text "tidy_holes =" <+> ppr tidy_holes ])
 -}
 
-       ; tidy_items <- mapM mkErrorItem tidy_cts
+       ; tidy_items <- mapMaybeM mkErrorItem tidy_cts
        ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples
                                          , text "Suppress =" <+> ppr (cec_suppress ctxt)
                                          , text "tidy_cts   =" <+> ppr tidy_cts
@@ -837,6 +843,43 @@ We use the `suppress` function within reportWanteds to filter out these two
 cases, then report all other errors. Lastly, we return to these suppressed
 ones and report them only if there have been no errors so far.
 
+Note [Constraints to ignore]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Some constraints are meant only to aid the solver by unification; a failure
+to solve them is not necessarily an error to report to the user. It is critical
+that compilation is aborted elsewhere if there are any ignored constraints here;
+they will remain unfilled, and might have been used to rewrite another constraint.
+
+Currently, the constraints to ignore are:
+
+1) Constraints generated in order to unify associated type instance parameters
+   with class parameters. Here are two illustrative examples:
+
+     class C (a :: k) where
+       type F (b :: k)
+
+     instance C True where
+       type F a = Int
+
+     instance C Left where
+       type F (Left :: a -> Either a b) = Bool
+
+   In the first instance, we want to infer that `a` has type Bool. So we emit
+   a constraint unifying kappa (the guessed type of `a`) with Bool. All is well.
+
+   In the second instance, we process the associated type instance only
+   after fixing the quantified type variables of the class instance. We thus
+   have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1).
+   Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so.
+   checkConsistentFamInst checks for this, and will fail if anything has gone
+   awry. Really the equality constraints emitted are just meant as an aid, not
+   a requirement. This is test case T13972.
+
+   We detect this case by looking for an origin of AssocFamPatOrigin; constraints
+   with this origin are dropped entirely during error message reporting.
+
+   If there is any trouble, checkValidFamInst bleats, aborting compilation.
+
 -}
 
 


=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -37,6 +37,8 @@ import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Solver
 import GHC.Tc.Types.Evidence
+import GHC.Tc.Types.Constraint
+import GHC.Core.Predicate
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
@@ -791,7 +793,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
-                    mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
+                    mapM (mkExport prag_fn residual insoluble qtvs inferred_theta) mono_infos
 
        ; loc <- getSrcSpanM
        ; let poly_ids = map abe_poly exports
@@ -808,6 +810,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
 
 --------------
 mkExport :: TcPragEnv
+         -> WantedConstraints  -- residual constraints, already emitted (for errors only)
          -> Bool                        -- True <=> there was an insoluble type error
                                         --          when typechecking the bindings
          -> [TyVar] -> TcThetaType      -- Both already zonked
@@ -826,12 +829,12 @@ mkExport :: TcPragEnv
 
 -- Pre-condition: the qtvs and theta are already zonked
 
-mkExport prag_fn insoluble qtvs theta
+mkExport prag_fn residual insoluble qtvs theta
          mono_info@(MBI { mbi_poly_name = poly_name
                         , mbi_sig       = mb_sig
                         , mbi_mono_id   = mono_id })
   = do  { mono_ty <- zonkTcType (idType mono_id)
-        ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
+        ; poly_id <- mkInferredPolyId residual insoluble qtvs theta poly_name mb_sig mono_ty
 
         -- NB: poly_id has a zonked type
         ; poly_id <- addInlinePrags poly_id prag_sigs
@@ -867,12 +870,13 @@ mkExport prag_fn insoluble qtvs theta
     prag_sigs = lookupPragEnv prag_fn poly_name
     sig_ctxt  = InfSigCtxt poly_name
 
-mkInferredPolyId :: Bool  -- True <=> there was an insoluble error when
+mkInferredPolyId :: WantedConstraints   -- the residual constraints, already emitted
+                 -> Bool  -- True <=> there was an insoluble error when
                           --          checking the binding group for this Id
                  -> [TyVar] -> TcThetaType
                  -> Name -> Maybe TcIdSigInst -> TcType
                  -> TcM TcId
-mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
+mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
   | Just (TISI { sig_inst_sig = sig })  <- mb_sig_inst
   , CompleteSig { sig_bndr = poly_id } <- sig
   = return poly_id
@@ -893,7 +897,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
                -- We can discard the coercion _co, because we'll reconstruct
                -- it in the call to tcSubType below
 
-       ; (binders, theta') <- chooseInferredQuantifiers inferred_theta
+       ; (binders, theta') <- chooseInferredQuantifiers residual inferred_theta
                                 (tyCoVarsOfType mono_ty') qtvs mb_sig_inst
 
        ; let inferred_poly_ty = mkForAllTys binders (mkPhiTy theta' mono_ty')
@@ -911,12 +915,13 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
        ; return (mkLocalId poly_name inferred_poly_ty) }
 
 
-chooseInferredQuantifiers :: TcThetaType   -- inferred
+chooseInferredQuantifiers :: WantedConstraints  -- residual constraints
+                          -> TcThetaType   -- inferred
                           -> TcTyVarSet    -- tvs free in tau type
                           -> [TcTyVar]     -- inferred quantified tvs
                           -> Maybe TcIdSigInst
                           -> TcM ([TyVarBinder], TcThetaType)
-chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
+chooseInferredQuantifiers _residual inferred_theta tau_tvs qtvs Nothing
   = -- No type signature (partial or complete) for this binder,
     do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
                         -- Include kind variables!  #7916
@@ -926,11 +931,11 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
                         , tv `elemVarSet` free_tvs ]
        ; return (binders, my_theta) }
 
-chooseInferredQuantifiers inferred_theta tau_tvs qtvs
-                          (Just (TISI { sig_inst_sig   = sig  -- Always PartialSig
-                                      , sig_inst_wcx   = wcx
-                                      , sig_inst_theta = annotated_theta
-                                      , sig_inst_skols = annotated_tvs }))
+chooseInferredQuantifiers residual inferred_theta tau_tvs qtvs
+  (Just (TISI { sig_inst_sig   = sig@(PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty })
+              , sig_inst_wcx   = wcx
+              , sig_inst_theta = annotated_theta
+              , sig_inst_skols = annotated_tvs }))
   = -- Choose quantifiers for a partial type signature
     do { psig_qtv_prs <- zonkTyVarTyVarPairs annotated_tvs
 
@@ -943,8 +948,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
             -- signature is not actually quantified.  How can that happen?
             -- See Note [Quantification and partial signatures] Wrinkle 4
             --     in GHC.Tc.Solver
-       ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
-                                          , not (tv `elem` qtvs) ]
+       ; mapM_ report_mono_sig_tv_err [ pr | pr@(_,tv) <- psig_qtv_prs
+                                           , not (tv `elem` qtvs) ]
 
        ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs)
 
@@ -961,22 +966,28 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
        ; return (final_qtvs, my_theta) }
   where
     report_dup_tyvar_tv_err (n1,n2)
-      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
       = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
                         <+> text "with" <+> quotes (ppr n2))
                      2 (hang (text "both bound by the partial type signature:")
                            2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
 
-      | otherwise -- Can't happen; by now we know it's a partial sig
-      = pprPanic "report_tyvar_tv_err" (ppr sig)
-
-    report_mono_sig_tv_err n
-      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
+    report_mono_sig_tv_err (n,tv)
       = addErrTc (hang (text "Can't quantify over" <+> quotes (ppr n))
-                     2 (hang (text "bound by the partial type signature:")
-                           2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
-      | otherwise -- Can't happen; by now we know it's a partial sig
-      = pprPanic "report_mono_sig_tv_err" (ppr sig)
+                     2 (vcat [ hang (text "bound by the partial type signature:")
+                                  2 (ppr fn_name <+> dcolon <+> ppr hs_ty)
+                             , extra ]))
+      where
+        extra | rhs_ty:_ <- [ rhs
+                               -- recall that residuals are always implications
+                            | residual_implic <- bagToList $ wc_impl residual
+                            , residual_ct <- bagToList $ wc_simple (ic_wanted residual_implic)
+                            , let residual_pred = ctPred residual_ct
+                            , Just (Nominal, lhs, rhs) <- [ getEqPredTys_maybe residual_pred ]
+                            , Just lhs_tv <- [ tcGetTyVar_maybe lhs ]
+                            , lhs_tv == tv ]
+              = sep [ quotes (ppr n), text "should really be", quotes (ppr rhs_ty) ]
+              | otherwise
+              = empty
 
     choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
                         -> TcM (VarSet, TcThetaType)
@@ -1021,6 +1032,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
        -- Hack alert!  See GHC.Tc.Gen.HsType:
        -- Note [Extra-constraint holes in partial type signatures]
 
+chooseInferredQuantifiers _ _ _ _ (Just (TISI { sig_inst_sig = sig@(CompleteSig {}) }))
+  = pprPanic "chooseInferredQuantifiers" (ppr sig)
 
 mk_impedance_match_msg :: MonoBindInfo
                        -> TcType -> TcType


=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -1730,7 +1730,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
        ; tau <- zonkTcType tau
        ; let inferred_theta = map evVarPred givens
              tau_tvs        = tyCoVarsOfType tau
-       ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
+       ; (binders, my_theta) <- chooseInferredQuantifiers residual inferred_theta
                                    tau_tvs qtvs (Just sig_inst)
        ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
              my_sigma       = mkForAllTys binders (mkPhiTy  my_theta tau)


=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -131,10 +131,8 @@ matchGlobalInst :: DynFlags
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
 matchGlobalInst dflags short_cut clas tys
-  | cls_name == knownNatClassName
-  = matchKnownNat    dflags short_cut clas tys
-  | cls_name == knownSymbolClassName
-  = matchKnownSymbol dflags short_cut clas tys
+  | cls_name == knownNatClassName     = matchKnownNat    dflags short_cut clas tys
+  | cls_name == knownSymbolClassName  = matchKnownSymbol dflags short_cut clas tys
   | isCTupleClass clas                = matchCTuple          clas tys
   | cls_name == typeableClassName     = matchTypeable        clas tys
   | clas `hasKey` heqTyConKey         = matchHeteroEquality       tys


=====================================
compiler/GHC/Tc/Instance/Family.hs
=====================================
@@ -162,9 +162,7 @@ addressed yet.
 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
 -- Freshen the type variables of the FamInst branches
 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
-  = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
-    ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
-    -- We used to have an assertion that the tyvars of the RHS were bound
+  = -- We used to have an assertion that the tyvars of the RHS were bound
     -- by tcv_set, but in error situations like  F Int = a that isn't
     -- true; a later check in checkValidFamInst rejects it
     do { (subst, tvs') <- freshenTyVarBndrs tvs
@@ -199,10 +197,6 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
                          , fi_rhs      = rhs'
                          , fi_axiom    = axiom }) }
   where
-    lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
-    rhs_kind = tcTypeKind rhs
-    tcv_set  = mkVarSet (tvs ++ cvs)
-    pp_ax    = pprCoAxiom axiom
     CoAxBranch { cab_tvs = tvs
                , cab_cvs = cvs
                , cab_lhs = lhs


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1147,7 +1147,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
                -- we want to find any other variables that are determined by this
                -- set, by functional dependencies or equalities. We thus use
                -- oclose to find all further variables determined by this root
-               -- set.
+               -- set. "RAE" update comments
 
              mono_tvs2 = oclose candidates mono_tvs1
 
@@ -1382,7 +1382,7 @@ pickQuantifiablePreds qtvs theta
         && (checkValidClsArgs flex_ctxt cls tys)
            -- Only quantify over predicates that checkValidType
            -- will pass!  See #10351.
-        && (no_fixed_dependencies cls tys)
+        && (no_fixed_dependencies cls tys) -- "RAE": comment this line
 
     no_fixed_dependencies cls tys
       = and [ qtvs `intersectsVarSet` tyCoVarsOfTypes fd_lhs_tys
@@ -2585,11 +2585,15 @@ floatConstraints skols given_ids ev_binds_var no_given_eqs
           -- in GHC.Tc.Solver.Monad
       ClassPred cls args
         | isIPClass cls
-        , [ip_name_strty, _ty] <- args
-        , Just ip_name <- isStrLitTy ip_name_strty
-        -> not (ip_name `elementOfUniqSet` given_ip_names)
+        , [ip_name_strty, ip_ty] <- args
+        , Just ip_name <- isStrLitTy ip_name_strty  -- should always succeed
+        -> not (isCallStackTy ip_ty) &&   -- don't float HasCallStack, as this will always be solved
+                                          -- See Note [Overview of implicit CallStacks]
+                                          -- in GHC.Tc.Types.Evidence
+           not (ip_name `elementOfUniqSet` given_ip_names)
 
         | otherwise      -> classHasFds cls
+
       _               -> False
 
     -- The set of implicit parameters bound in the enclosing implication


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -168,6 +168,7 @@ canClassNC ev cls tys
                             -- We change the origin to IPOccOrigin so
                             -- this rule does not fire again.
                             -- See Note [Overview of implicit CallStacks]
+                            -- in GHC.Tc.Types.Evidence
 
        ; new_ev <- newWantedEvVarNC new_loc rewriters pred
 
@@ -1600,7 +1601,25 @@ representational role]. See #10534 and test case
 typecheck/should_fail/T10534.
 
 {4}: Because type variables can stand in for newtypes, we conservatively do not
-decompose AppTys over representational equality.
+decompose AppTys over representational equality. Here are two examples that
+demonstrate why we can't:
+
+   4a: newtype Phant a = MkPhant Int
+       [W] alpha Int ~R beta Bool
+
+   If we eventually solve alpha := Phant and beta := Phant, then we can solve
+   this equality by unwrapping. But it would have been disastrous to decompose
+   the wanted to produce Int ~ Bool, which is definitely insoluble.
+
+   4b: newtype Age = MkAge Int
+       [W] alpha Age ~R Maybe Int
+
+   First, a question: if we know that ty1 ~R ty2, can we conclude that
+   a ty1 ~R a ty2? Not for all a. This is precisely why we need role annotations
+   on type constructors. So, if we were to decompose, we would need to
+   decompose to [W] alpha ~R Maybe and [W] Age ~ Int. On the other hand, if we
+   later solve alpha := Maybe, then we would decompose to [W] Age ~R Int, and
+   that would be soluble.
 
 In the implementation of can_eq_nc and friends, we don't directly pattern
 match using lines like in the tables above, as those tables don't cover


=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -2970,7 +2970,8 @@ addConsistencyConstraints mb_clsinfo fam_app
                    , Just cls_ty <- [lookupVarEnv inst_env fam_tc_tv] ]
        ; traceTc "addConsistencyConstraints" (ppr eqs)
        ; emitDerivedEqs AssocFamPatOrigin eqs }
-    -- Improve inference
+    -- Improve inference; these equalities will not produce errors.
+    -- See Note [Constraints to ignore] in GHC.Tc.Errors
     -- Any mis-match is reports by checkConsistentFamInst
   | otherwise
   = return ()


=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -372,6 +372,8 @@ data CtOrigin
   | ArithSeqOrigin (ArithSeqInfo GhcRn) -- [x..], [x..y] etc
   | AssocFamPatOrigin   -- When matching the patterns of an associated
                         -- family instance with that of its parent class
+                        -- IMPORTANT: These constraints will never cause errors;
+                        -- See Note [Constraints to ignore] in GHC.Tc.Errors
   | SectionOrigin
   | TupleOrigin         -- (..,..)
   | ExprSigOrigin       -- e :: ty


=====================================
compiler/GHC/Tc/Utils/Zonk.hs
=====================================
@@ -1833,11 +1833,6 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
               -- (undeferred) type errors. Originally, I put in a panic
               -- here, but that caused too many uses of `failIfErrsM`.
            Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr hole)
-                         ; when debugIsOn $
-                           whenNoErrs $
-                           MASSERT2( False
-                                   , text "Type-correct unfilled coercion hole"
-                                     <+> ppr hole )
                          ; cv' <- zonkCoVar cv
                          ; return $ mkCoVarCo cv' } }
                              -- This will be an out-of-scope variable, but keeping


=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -826,7 +826,6 @@ For further reading, see:
 
 Note [Bangs on imported data constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 We pass Maybe [HsImplBang] to mkDataConRep to make use of HsImplBangs
 from imported modules.
 


=====================================
testsuite/tests/dependent/should_compile/all.T
=====================================
@@ -66,3 +66,4 @@ test('T16326_Compile2', normal, compile, [''])
 test('T16391a', normal, compile, [''])
 test('T16344b', normal, compile, [''])
 test('T16347', normal, compile, [''])
+test('LopezJuan', normal, compile, [''])


=====================================
testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
=====================================
@@ -1,29 +1,27 @@
 
 PushedInAsGivens.hs:10:31: error:
-    • Could not deduce: a1 ~ a
-      from the context: F Int ~ [a1]
+    • Could not deduce: a ~ a0
+      from the context: F Int ~ [a]
         bound by the type signature for:
-                   foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
+                   foo :: forall a. (F Int ~ [a]) => a -> Int
         at PushedInAsGivens.hs:9:13-44
-      ‘a1’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the type signature for:
-          foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
+          foo :: forall a. (F Int ~ [a]) => a -> 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]
     • Relevant bindings include
-        x :: a1 (bound at PushedInAsGivens.hs:10:17)
-        foo :: a1 -> Int (bound at PushedInAsGivens.hs:10:13)
-        y :: a (bound at PushedInAsGivens.hs:9:5)
-        bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
+        x :: a (bound at PushedInAsGivens.hs:10:17)
+        foo :: a -> Int (bound at PushedInAsGivens.hs:10:13)
+        y :: a0 (bound at PushedInAsGivens.hs:9:5)
+        bar :: a0 -> (a0, Int) (bound at PushedInAsGivens.hs:9:1)
 
 PushedInAsGivens.hs:11:15: error:
-    • Couldn't match type ‘F Int’ with ‘[a]’
+    • Couldn't match type ‘F Int’ with ‘[a0]’
         arising from a use of ‘foo’
+      The type variable ‘a0’ is ambiguous
     • In the expression: foo y
       In the expression: (y, foo y)
       In the expression:
@@ -32,5 +30,5 @@ PushedInAsGivens.hs:11:15: error:
           foo x = length [...]
         in (y, foo y)
     • Relevant bindings include
-        y :: a (bound at PushedInAsGivens.hs:9:5)
-        bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
+        y :: a0 (bound at PushedInAsGivens.hs:9:5)
+        bar :: a0 -> (a0, Int) (bound at PushedInAsGivens.hs:9:1)


=====================================
testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
=====================================
@@ -1,12 +1,13 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[p0]’
+      The type variable ‘p0’ is ambiguous
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: p (bound at ExtraTcsUntch.hs:21:3)
-        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: p0 (bound at ExtraTcsUntch.hs:21:3)
+        f :: p0 -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
     • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’


=====================================
testsuite/tests/indexed-types/should_fail/T13972.hs
=====================================
@@ -8,7 +8,7 @@ import Data.Kind
 class C (a :: k) where
   type T k :: Type
 
--- This used to fail, with a mysterious error messate
+-- This used to fail, with a mysterious error message
 --    Type indexes must match class instance head
 --      Expected: T (a1 -> Either a1 b1)
 --      Actual: T (a -> Either a b)


=====================================
testsuite/tests/indexed-types/should_fail/T14230a.stderr
=====================================
@@ -1,6 +1,7 @@
 
-T14230a.hs:13:14: error:
-    • Expected kind ‘k -> *’, but ‘a’ has kind ‘*’
-    • In the second argument of ‘CD’, namely ‘(a :: k -> *)’
-      In the data instance declaration for ‘CD’
+T14230a.hs:13:3: error:
+    • Type indexes must match class instance head
+      Expected: CD (*) (Maybe a)
+        Actual: CD k a
+    • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C (Maybe a)’


=====================================
testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
=====================================
@@ -17,23 +17,11 @@ NamedWildcardExplicitForall.hs:10:8: error:
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: bar :: _a -> _a
 
-NamedWildcardExplicitForall.hs:13:26: error:
-    • Found type wildcard ‘_b’ standing for ‘Bool’
-      To use the inferred type, enable PartialTypeSignatures
-    • In the type signature: baz :: forall _a. _a -> _b -> (_a, _b)
-
-NamedWildcardExplicitForall.hs:14:16: error:
-    • Couldn't match expected type ‘Bool’ with actual type ‘_a’
-      ‘_a’ is a rigid type variable bound by
-        the inferred type of baz :: _a -> Bool -> (_a, Bool)
-        at NamedWildcardExplicitForall.hs:13:15-16
-    • In the first argument of ‘not’, namely ‘x’
-      In the expression: not x
-      In the expression: (not x, not y)
-    • Relevant bindings include
-        x :: _a (bound at NamedWildcardExplicitForall.hs:14:5)
-        baz :: _a -> Bool -> (_a, Bool)
-          (bound at NamedWildcardExplicitForall.hs:14:1)
+NamedWildcardExplicitForall.hs:14:1: error:
+    Can't quantify over ‘_a’
+      bound by the partial type signature:
+        baz :: forall _a. _a -> _b -> (_a, _b)
+      ‘_a’ should really be ‘Bool’
 
 NamedWildcardExplicitForall.hs:16:8: error:
     • Found type wildcard ‘_a’ standing for ‘Bool’


=====================================
testsuite/tests/polykinds/T14172.stderr
=====================================
@@ -24,15 +24,3 @@ T14172.hs:7:19: error:
     • Relevant bindings include
         traverseCompose :: (a -> f b) -> g a -> f (h a')
           (bound at T14172.hs:7:1)
-
-T14172.hs:7:19: error:
-    • Couldn't match type ‘Compose f'0 g'1 a'0 -> f (h a')’
-                     with ‘g a -> f (h a')’
-      Expected type: (a -> f b) -> g a -> f (h a')
-        Actual type: (a -> f b) -> Compose f'0 g'1 a'0 -> f (h a')
-    • In the expression: _Wrapping Compose . traverse
-      In an equation for ‘traverseCompose’:
-          traverseCompose = _Wrapping Compose . traverse
-    • Relevant bindings include
-        traverseCompose :: (a -> f b) -> g a -> f (h a')
-          (bound at T14172.hs:7:1)


=====================================
testsuite/tests/th/T11452.stderr
=====================================
@@ -9,7 +9,6 @@ T11452.hs:6:12: error:
 T11452.hs:6:14: error:
     • Cannot instantiate unification variable ‘p0’
       with a type involving polytypes: forall a. a -> a
-        GHC doesn't yet support impredicative polymorphism
     • In the Template Haskell quotation [|| \ _ -> () ||]
       In the expression: [|| \ _ -> () ||]
       In the Template Haskell splice $$([|| \ _ -> () ||])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f550eed809836699a98f67220baaf980bc08dcb9

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f550eed809836699a98f67220baaf980bc08dcb9
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200918/427a6d85/attachment-0001.html>


More information about the ghc-commits mailing list