diff options
Diffstat (limited to 'compiler/GHC/Tc/Errors.hs')
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 54 |
1 files changed, 33 insertions, 21 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 3a77998c8f..f3c8a19b04 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -19,9 +19,9 @@ import GHC.Tc.Utils.Monad import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Utils.TcMType -import GHC.Tc.Utils.Unify( occCheckForErrors, CheckTyEqResult(..) ) import GHC.Tc.Utils.Env( tcInitTidyEnv ) import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Unify ( checkTyVarEq ) import GHC.Tc.Types.Origin import GHC.Rename.Unbound ( unknownNameSuggestions, WhatLooking(..) ) import GHC.Core.Type @@ -600,10 +600,10 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] - -- also checks to make sure the constraint isn't BlockedCIS + -- also checks to make sure the constraint isn't HoleBlockerReason -- See TcCanonical Note [Equalities with incompatible kinds], (4) unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool - unblocked _ (CIrredCan { cc_status = BlockedCIS {}}) _ = False + unblocked _ (CIrredCan { cc_reason = HoleBlockerReason {}}) _ = False unblocked checker ct pred = checker ct pred -- rigid_nom_eq, rigid_nom_tv_eq, @@ -1544,6 +1544,22 @@ mkTyVarEqErr ctxt report ct tv1 ty2 mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct -> TcTyVar -> TcType -> Report mkTyVarEqErr' dflags ctxt report ct tv1 ty2 + -- impredicativity is a simple error to understand; try it first + | check_eq_result `cterHasProblem` cteImpredicative + = let msg = vcat [ (if isSkolemTyVar tv1 + then text "Cannot equate type variable" + else text "Cannot instantiate unification variable") + <+> quotes (ppr tv1) + , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ] + in + -- Unlike the other reports, this discards the old 'report_important' + -- instead of augmenting it. This is because the details are not likely + -- to be helpful since this is just an unimplemented feature. + mconcat [ headline_msg + , important msg + , if isSkolemTyVar tv1 then extraTyVarEqInfo ctxt tv1 ty2 else mempty + , report ] + | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) @@ -1555,11 +1571,10 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 , report ] - | CTE_Occurs <- occ_check_expand + | cterHasOccursCheck check_eq_result -- We report an "occurs check" even for a ~ F t a, where F is a type -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it - -- See Note [Occurs check error] in GHC.Tc.Solver.Canonical = let extra2 = mkEqInfoMsg ct ty1 ty2 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $ @@ -1576,16 +1591,6 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 in mconcat [headline_msg, extra2, extra3, report] - | CTE_Bad <- occ_check_expand - = let msg = vcat [ text "Cannot instantiate unification variable" - <+> quotes (ppr tv1) - , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ] - in - -- Unlike the other reports, this discards the old 'report_important' - -- instead of augmenting it. This is because the details are not likely - -- to be helpful since this is just an unimplemented feature. - mconcat [ headline_msg, important msg, report ] - -- If the immediately-enclosing implication has 'tv' a skolem, and -- we know by now its an InferSkol kind of skolem, then presumably -- it started life as a TyVarTv, else it'd have been unified, given @@ -1647,15 +1652,24 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 | otherwise = reportEqErr ctxt report ct (mkTyVarTy tv1) ty2 - -- This *can* happen (#6123, and test T2627b) + -- This *can* happen (#6123) -- Consider an ambiguous top-level constraint (a ~ F a) -- Not an occurs check, because F is a type function. where headline_msg = misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2 ty1 = mkTyVarTy tv1 - occ_check_expand = occCheckForErrors dflags tv1 ty2 - insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2 + + check_eq_result = case ct of + CIrredCan { cc_reason = NonCanonicalReason result } -> result + CIrredCan { cc_reason = HoleBlockerReason {} } -> cteProblem cteHoleBlocker + _ -> checkTyVarEq dflags tv1 ty2 + -- in T2627b, we report an error for F (F a0) ~ a0. Note that the type + -- variable is on the right, so we don't get useful info for the CIrredCan, + -- and have to compute the result of checkTyVarEq here. + + + insoluble_occurs_check = check_eq_result `cterHasProblem` cteInsolubleOccurs what = text $ levelString $ ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel @@ -2073,8 +2087,6 @@ pprWithExplicitKindsWhenMismatch ty1 ty2 ct -- True when the visible bit of the types look the same, -- so we want to show the kinds in the displayed type - - {- Note [Insoluble occurs check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble @@ -2085,7 +2097,7 @@ we don't solve it from the Given. It's very confusing to say And indeed even thinking about the Givens is silly; [W] a ~ [a] is just as insoluble as Int ~ Bool. -Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck) +Conclusion: if there's an insoluble occurs check (cteInsolubleOccurs) then report it directly, not in the "cannot deduce X from Y" form. This is done in misMatchOrCND (via the insoluble_occurs_check arg) |