Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

14 changed files:

Changes:

  • compiler/GHC/Core/Predicate.hs
    ... ... @@ -217,7 +217,7 @@ in GHC.Tc.Solver.Dict.
    217 217 
     -- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
    218 218 
     isEqPred :: PredType -> Bool
    219 219 
     -- True of (s ~# t) (s ~R# t)
    220 
    --- NB: but NOT true of (s ~ t) or (s ~~ t) or (Coecible s t)
    220 
    +-- NB: but NOT true of (s ~ t) or (s ~~ t) or (Coercible s t)
    221 221 
     isEqPred ty
    222 222 
       | Just tc <- tyConAppTyCon_maybe ty
    223 223 
       = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey

  • compiler/GHC/Core/Type.hs
    ... ... @@ -74,8 +74,7 @@ module GHC.Core.Type (
    74 74
    75 75 
             mkCastTy, mkCoercionTy, splitCastTy_maybe,
    76 76
    77 
    -        ErrorMsgType,
    78 
    -        userTypeError_maybe, deepUserTypeError_maybe, pprUserTypeErrorTy,
    77 
    +        ErrorMsgType, pprUserTypeErrorTy,
    79 78
    80 79 
             coAxNthLHS,
    81 80 
             stripCoercionTy,
    ... ... @@ -272,7 +271,7 @@ import GHC.Utils.Outputable
    272 271 
     import GHC.Utils.Panic
    273 272 
     import GHC.Data.FastString
    274 273
    275 
    -import GHC.Data.Maybe   ( orElse, isJust, firstJust )
    274 
    +import GHC.Data.Maybe   ( orElse, isJust )
    276 275 
     import GHC.List (build)
    277 276
    278 277 
     -- $type_classification
    ... ... @@ -1223,45 +1222,6 @@ isLitTy ty
    1223 1222 
     -- | A type of kind 'ErrorMessage' (from the 'GHC.TypeError' module).
    1224 1223 
     type ErrorMsgType = Type
    1225 1224
    1226 
    --- | Is this type a custom user error?
    1227 
    --- If so, give us the error message.
    1228 
    -userTypeError_maybe :: Type -> Maybe ErrorMsgType
    1229 
    -userTypeError_maybe ty
    1230 
    -  | Just ty' <- coreView ty = userTypeError_maybe ty'
    1231 
    -userTypeError_maybe (TyConApp tc (_kind : msg : _))
    1232 
    -  | tyConName tc == errorMessageTypeErrorFamName
    1233 
    -          -- There may be more than 2 arguments, if the type error is
    1234 
    -          -- used as a type constructor (e.g. at kind `Type -> Type`).
    1235 
    -  = Just msg
    1236 
    -userTypeError_maybe _
    1237 
    -  = Nothing
    1238 
    -
    1239 
    -deepUserTypeError_maybe :: Type -> Maybe ErrorMsgType
    1240 
    --- Look for custom user error, deeply inside the type
    1241 
    -deepUserTypeError_maybe ty
    1242 
    -  | Just ty' <- coreView ty = userTypeError_maybe ty'
    1243 
    -deepUserTypeError_maybe (TyConApp tc tys)
    1244 
    -  | tyConName tc == errorMessageTypeErrorFamName
    1245 
    -  , _kind : msg : _ <- tys
    1246 
    -          -- There may be more than 2 arguments, if the type error is
    1247 
    -          -- used as a type constructor (e.g. at kind `Type -> Type`).
    1248 
    -  = Just msg
    1249 
    -
    1250 
    -  | tyConMustBeSaturated tc  -- Don't go looking for user type errors
    1251 
    -                             -- inside type family arguments (see #20241).
    1252 
    -  = foldr (firstJust . deepUserTypeError_maybe) Nothing (drop (tyConArity tc) tys)
    1253 
    -  | otherwise
    1254 
    -  = foldr (firstJust . deepUserTypeError_maybe) Nothing tys
    1255 
    -deepUserTypeError_maybe (ForAllTy _ ty) = deepUserTypeError_maybe ty
    1256 
    -deepUserTypeError_maybe (FunTy { ft_arg = arg, ft_res = res })
    1257 
    -  = deepUserTypeError_maybe arg `firstJust` deepUserTypeError_maybe res
    1258 
    -deepUserTypeError_maybe (AppTy t1 t2)
    1259 
    -  = deepUserTypeError_maybe t1 `firstJust` deepUserTypeError_maybe t2
    1260 
    -deepUserTypeError_maybe (CastTy ty _)
    1261 
    -  = deepUserTypeError_maybe ty
    1262 
    -deepUserTypeError_maybe _   -- TyVarTy, CoercionTy, LitTy
    1263 
    -  = Nothing
    1264 
    -
    1265 1225 
     -- | Render a type corresponding to a user type error into a SDoc.
    1266 1226 
     pprUserTypeErrorTy :: ErrorMsgType -> SDoc
    1267 1227 
     pprUserTypeErrorTy ty =

  • compiler/GHC/Tc/Errors.hs
    ... ... @@ -671,11 +671,14 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    671 671 
         non_tv_eq _ _                    = False
    672 672
    673 673 
         -- Catch TypeError and Unsatisfiable.
    674 
    -    -- Here, we want any nested TypeErrors to bubble up, so we use
    675 
    -    -- 'containsUserTypeError' and not 'isTopLevelUserTypeError'.
    674 
    +    -- Here, we want any nested TypeErrors to bubble up, even if they are
    675 
    +    -- inside type family applications, so we pass 'True' to
    676 
    +    -- 'containsUserTypeError'.
    676 677 
         --
    677 678 
         -- See also Note [Implementation of Unsatisfiable constraints], point (F).
    678 
    -    is_user_type_error item _ = containsUserTypeError (errorItemPred item)
    679 
    +    is_user_type_error item _ = containsUserTypeError True (errorItemPred item)
    680 
    +      -- True <=> look under ty-fam apps, AppTy etc.
    681 
    +      -- See (UTE2) in Note [Custom type errors in constraints].
    679 682
    680 683 
         is_implicit_lifting item _ =
    681 684 
           case (errorItemOrigin item) of
    ... ... @@ -977,6 +980,8 @@ Its implementation consists of the following:
    977 980
    978 981 
          This is the only way that "Unsatisfiable msg" constraints are reported,
    979 982 
          which makes their behaviour much more predictable than TypeError.
    983 
    +     We don't go looking for Unsatisfiable constraints deeply nested inside
    984 
    +     a type like we do for TypeError.
    980 985 
     -}
    981 986
    982 987
    ... ... @@ -1124,12 +1129,21 @@ mkUserTypeErrorReporter ctxt
    1124 1129 
                             ; maybeReportError ctxt (item :| []) err
    1125 1130 
                             ; addSolverDeferredBinding err item }
    1126 1131
    1132 
    +
    1133 
    +
    1127 1134 
     mkUserTypeError :: ErrorItem -> TcSolverReportMsg
    1128 1135 
     mkUserTypeError item
    1129 
    -  | Just msg <- getUserTypeErrorMsg pty
    1130 
    -  = UserTypeError msg
    1131 1136 
       | Just msg <- isUnsatisfiableCt_maybe pty
    1132 1137 
       = UnsatisfiableError msg
    1138 
    +  | Just msg <- userTypeError_maybe True pty
    1139 
    +      --                            ^^^^
    1140 
    +      -- Look under type-family applications! We are reporting an error,
    1141 
    +      -- so we may as well look to see if there are any custom type errors
    1142 
    +      -- anywhere, as they might be helpful to the user. We gave the type
    1143 
    +      -- family application the chance to reduce, but it didn't.
    1144 
    +      --
    1145 
    +      -- See (UTE2) in Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint.
    1146 
    +  = UserTypeError msg
    1133 1147 
       | otherwise
    1134 1148 
       = pprPanic "mkUserTypeError" (ppr item)
    1135 1149 
       where

  • compiler/GHC/Tc/Solver.hs
    ... ... @@ -659,20 +659,70 @@ equality constraint, but it is also important to detect custom type errors:
    659 659
    660 660 
     To see that we can't call `foo (MkT2)`, we must detect that `NotInt Int` is insoluble
    661 661 
     because it is a custom type error.
    662 
    -Failing to do so proved quite inconvenient for users, as evidence by the
    662 
    +Failing to do so proved quite inconvenient for users, as evidenced by the
    663 663 
     tickets #11503 #14141 #16377 #20180.
    664 664 
     Test cases: T11503, T14141.
    665 665
    666 
    -Examples of constraints that tcCheckGivens considers insoluble:
    666 
    +To do this, tcCheckGivens calls getInertInsols, which returns all Given
    667 
    +constraints that are definitely insoluble. See Note [When is a constraint insoluble?].
    668 
    +
    669 
    +Note [When is a constraint insoluble?]
    670 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    671 
    +Whether a constraint is insoluble matters for accurate pattern-match
    672 
    +warnings, as explained in Note [Pattern match warnings with insoluble Givens].
    673 
    +
    674 
    +We consider a constraint to be insoluble if it definitely cannot be solved,
    675 
    +no matter what information we might further discover. For example, the following
    676 
    +constraints are insoluble:
    677 
    +
    667 678 
       - Int ~ Bool,
    668 679 
       - Coercible Float Word,
    669 
    -  - TypeError msg.
    670 
    -
    671 
    -Non-examples:
    672 
    -  - constraints which we know aren't satisfied,
    673 
    -    e.g. Show (Int -> Int) when no such instance is in scope,
    674 
    -  - Eq (TypeError msg),
    675 
    -  - C (Int ~ Bool), with @class C (c :: Constraint)@.
    680 
    +  - TypeError msg
    681 
    +  - TypeError msg ~ Int
    682 
    +  - Unsatisfiable msg
    683 
    +
    684 
    +Many constraints that look like they can't be solved are in fact not reported
    685 
    +as insoluble, as there might still be a possibility (no matter how remote) that
    686 
    +they can still be solved:
    687 
    +
    688 
    +  1: Show (Int -> Int)
    689 
    +
    690 
    +  Reason: even though there is no relevant instance in scope, this constraint
    691 
    +  could later get solved by a new instance.
    692 
    +
    693 
    +  2: C (Int ~ Bool), where C :: Constraint -> Constraint
    694 
    +
    695 
    +  Reason: even though 'Int ~ Bool' is insoluble, the constraint 'C (Int ~ Bool)'
    696 
    +  might be soluble, e.g. if 'C' is a class and we have 'instance forall c. C c',
    697 
    +  or 'C' is a type family and we have 'type instance C c = (() :: Constraint)'.
    698 
    +
    699 
    +  3: Nested occurences of TypeError don't always lead to insolubility. For
    700 
    +     example, none of the following constraints are definitely insoluble:
    701 
    +
    702 
    +    (a) F alpha (TypeError msg)    -- 'F' is an arity 2 type family
    703 
    +    (b) Eq (TypeError msg)
    704 
    +    (c) c (TypeError msg)          -- 'c' is a metavariable
    705 
    +    (d) (TC alpha) (TypeError msg) -- 'TC' is an arity 1 type family
    706 
    +    (e) TypeError msg ~ rhs        -- (depends on rhs)
    707 
    +
    708 
    +  None of these constraints are definitely insoluble:
    709 
    +
    710 
    +    (a) Can be solved if 'F' reduces, e.g. 'alpha := Int', 'type instance F Int a = (() :: Constraint)'.
    711 
    +    (b) Can be solved by 'instance forall x. Eq x'.
    712 
    +    (c) Can be solved if 'c' unifies with 'C', as in example (2).
    713 
    +    (d) Can be solved if 'TC alpha' reduces to 'C', as in example (2).
    714 
    +    (e) If 'rhs' is a rigid type such as 'Int' or 'Maybe Char', then this
    715 
    +        constraint is definitely insoluble. Otherwise, however, the constraint
    716 
    +        could be soluble:
    717 
    +          - rhs = G alpha, for an arity 1 type family G
    718 
    +            G alpha could reduce to TypeError msg.
    719 
    +          - rhs = k, for a skolem type variable k.
    720 
    +            We could instantiate k to something else, and then the constraint
    721 
    +            could become soluble.
    722 
    +
    723 
    +  For this reason, we are careful to not pull out certain occurrences of TypeError,
    724 
    +  e.g. inside type family applications and class constraints.
    725 
    +  See Note [Custom type errors in constraints].
    676 726 
     -}
    677 727
    678 728 
     tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -172,7 +172,7 @@ import GHC.Tc.Types.Origin
    172 172 
     import GHC.Tc.Types.CtLoc
    173 173 
     import GHC.Tc.Types.Constraint
    174 174
    175 
    -import GHC.Builtin.Names ( unsatisfiableClassNameKey, callStackTyConName, exceptionContextTyConName )
    175 
    +import GHC.Builtin.Names ( callStackTyConName, exceptionContextTyConName )
    176 176
    177 177 
     import GHC.Core.Type
    178 178 
     import GHC.Core.TyCo.Rep as Rep
    ... ... @@ -185,6 +185,10 @@ import GHC.Core.Class
    185 185 
     import GHC.Core.TyCon
    186 186 
     import GHC.Core.Unify (typesAreApart)
    187 187
    188 
    +import GHC.LanguageExtensions as LangExt
    189 
    +import GHC.Rename.Env
    190 
    +import qualified GHC.Rename.Env as TcM
    191 
    +
    188 192 
     import GHC.Types.Name
    189 193 
     import GHC.Types.TyThing
    190 194 
     import GHC.Types.Name.Reader
    ... ... @@ -199,8 +203,7 @@ import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel)
    199 203 
     import GHC.Types.SrcLoc
    200 204
    201 205 
     import GHC.Unit.Module
    202 
    -import qualified GHC.Rename.Env as TcM
    203 
    -import GHC.Rename.Env
    206 
    +import GHC.Unit.Module.Graph
    204 207
    205 208 
     import GHC.Utils.Outputable
    206 209 
     import GHC.Utils.Panic
    ... ... @@ -220,15 +223,13 @@ import Data.List ( mapAccumL )
    220 223 
     import Data.List.NonEmpty ( nonEmpty )
    221 224 
     import qualified Data.List.NonEmpty as NE
    222 225 
     import qualified Data.Semigroup as S
    223 
    -import GHC.LanguageExtensions as LangExt
    226 
    +import qualified Data.Set as Set
    224 227
    225 228 
     #if defined(DEBUG)
    226 229 
     import GHC.Types.Unique.Set (nonDetEltsUniqSet)
    227 230 
     import GHC.Data.Graph.Directed
    228 231 
     #endif
    229 232
    230 
    -import qualified Data.Set as Set
    231 
    -import GHC.Unit.Module.Graph
    232 233
    233 234 
     {- *********************************************************************
    234 235 
     *                                                                      *
    ... ... @@ -666,9 +667,10 @@ getInnermostGivenEqLevel = do { inert <- getInertCans
    666 667 
     -- This consists of:
    667 668 
     --
    668 669 
     --  - insoluble equalities, such as @Int ~# Bool@;
    669 
    ---  - constraints that are top-level custom type errors, of the form
    670 
    ---    @TypeError msg@, but not constraints such as @Eq (TypeError msg)@
    671 
    ---    in which the type error is nested;
    670 
    +--  - constraints that are custom type errors, of the form
    671 
    +--    @TypeError msg@ or @Maybe (TypeError msg)@, but not constraints such as
    672 
    +--    @F x (TypeError msg)@ in which the type error is nested under
    673 
    +--    a type family application,
    672 674 
     --  - unsatisfiable constraints, of the form @Unsatisfiable msg@.
    673 675 
     --
    674 676 
     -- The inclusion of Givens is important for pattern match warnings, as we
    ... ... @@ -676,21 +678,26 @@ getInnermostGivenEqLevel = do { inert <- getInertCans
    676 678 
     -- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver).
    677 679 
     getInertInsols :: TcS Cts
    678 680 
     getInertInsols
    679 
    -  = do { inert <- getInertCans
    680 
    -       ; let insols = filterBag insolubleIrredCt (inert_irreds inert)
    681 
    -             unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey
    682 
    -       ; return $ fmap CDictCan unsats `unionBags` fmap CIrredCan insols }
    681 
    +  -- See Note [When is a constraint insoluble?]
    682 
    +  = do { inert_cts <- getInertCts
    683 
    +       ; return $ filterBag insolubleCt inert_cts }
    684 
    +
    685 
    +getInertCts :: TcS Cts
    686 
    +getInertCts
    687 
    +  = do { inerts <- getInertCans
    688 
    +       ; return $
    689 
    +          unionManyBags
    690 
    +            [ fmap CIrredCan $ inert_irreds inerts
    691 
    +            , foldDicts  (consBag . CDictCan) (inert_dicts  inerts) emptyBag
    692 
    +            , foldFunEqs (consBag . CEqCan  ) (inert_funeqs inerts) emptyBag
    693 
    +            , foldTyEqs  (consBag . CEqCan  ) (inert_eqs    inerts) emptyBag
    694 
    +            ] }
    683 695
    684 696 
     getInertGivens :: TcS [Ct]
    685 697 
     -- Returns the Given constraints in the inert set
    686 698 
     getInertGivens
    687 
    -  = do { inerts <- getInertCans
    688 
    -       ; let all_cts = foldIrreds ((:) . CIrredCan) (inert_irreds inerts)
    689 
    -                     $ foldDicts  ((:) . CDictCan)  (inert_dicts inerts)
    690 
    -                     $ foldFunEqs ((:) . CEqCan)    (inert_funeqs inerts)
    691 
    -                     $ foldTyEqs  ((:) . CEqCan)    (inert_eqs inerts)
    692 
    -                     $ []
    693 
    -       ; return (filter isGivenCt all_cts) }
    699 
    +  = do { all_cts <- getInertCts
    700 
    +       ; return (filter isGivenCt $ bagToList all_cts) }
    694 701
    695 702 
     getPendingGivenScs :: TcS [Ct]
    696 703 
     -- Find all inert Given dictionaries, or quantified constraints, such that

  • compiler/GHC/Tc/Solver/Solve.hs
    ... ... @@ -471,7 +471,9 @@ findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens
    471 471 
           | otherwise        = filterOut is_minimal givens
    472 472
    473 473 
         -- See #15232
    474 
    -    is_type_error id = isTopLevelUserTypeError (idType id)
    474 
    +    is_type_error id = containsUserTypeError False (idType id)
    475 
    +      -- False <=> do not look under ty-fam apps, AppTy etc.
    476 
    +      -- See (UTE1) in Note [Custom type errors in constraints].
    475 477
    476 478 
         is_improving pred -- (transSuperClasses p) does not include p
    477 479 
           = any isImprovementPred (pred : transSuperClasses pred)

  • compiler/GHC/Tc/Types/Constraint.hs
    1 1 
     {-# LANGUAGE DerivingStrategies #-}
    2 2 
     {-# LANGUAGE DuplicateRecordFields #-}
    3 3 
     {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    4 
    +{-# LANGUAGE MultiWayIf #-}
    4 5 
     {-# LANGUAGE TypeApplications #-}
    5 6
    6 7 
     -- | This module defines types and simple operations over constraints, as used
    ... ... @@ -13,7 +14,7 @@ module GHC.Tc.Types.Constraint (
    13 14 
             isPendingScDictCt, isPendingScDict, pendingScDict_maybe,
    14 15 
             superClassesMightHelp, getPendingWantedScs,
    15 16 
             isWantedCt, isGivenCt,
    16 
    -        isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg,
    17 
    +        userTypeError_maybe, containsUserTypeError,
    17 18 
             isUnsatisfiableCt_maybe,
    18 19 
             ctEvidence, updCtEvidence,
    19 20 
             ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
    ... ... @@ -59,7 +60,7 @@ module GHC.Tc.Types.Constraint (
    59 60 
             addInsols, dropMisleading, addSimples, addImplics, addHoles,
    60 61 
             addNotConcreteError, addMultiplicityCoercionError, addDelayedErrors,
    61 62 
             tyCoVarsOfWC, tyCoVarsOfWCList,
    62 
    -        insolubleWantedCt, insolubleCt, insolubleIrredCt,
    63 
    +        insolubleWantedCt, insolubleCt,
    63 64 
             insolubleImplic, nonDefaultableTyVarsOfWC,
    64 65 
             approximateWCX, approximateWC,
    65 66
    ... ... @@ -113,6 +114,7 @@ import GHC.Core.Coercion
    113 114 
     import GHC.Core.Class
    114 115 
     import GHC.Core.TyCon
    115 116 
     import GHC.Core.TyCo.Ppr
    117 
    +import GHC.Core.TyCo.Rep
    116 118
    117 119 
     import GHC.Types.Name
    118 120 
     import GHC.Types.Var
    ... ... @@ -136,16 +138,13 @@ import GHC.Utils.Constants (debugIsOn)
    136 138
    137 139 
     import GHC.Data.Bag
    138 140
    141 
    +import Control.Monad ( when )
    139 142 
     import Data.Coerce
    140 
    -import qualified Data.Semigroup as S
    141 
    -import Control.Monad ( msum, when )
    143 
    +import Data.List  ( intersperse )
    142 144 
     import Data.Maybe ( mapMaybe, isJust )
    143 
    -
    144 
    --- these are for CheckTyEqResult
    145 
    +import GHC.Data.Maybe ( firstJust, firstJusts )
    146 
    +import qualified Data.Semigroup as S
    145 147 
     import Data.Word  ( Word8 )
    146 
    -import Data.List  ( intersperse )
    147 
    -
    148 
    -
    149 148
    150 149 
     {-
    151 150 
     ************************************************************************
    ... ... @@ -1198,73 +1197,53 @@ insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors })
    1198 1197 
           is_insoluble (DE_Multiplicity {}) = False
    1199 1198
    1200 1199 
     insolubleWantedCt :: Ct -> Bool
    1201 
    --- Definitely insoluble, in particular /excluding/ type-hole constraints
    1202 
    --- Namely:
    1203 
    ---   a) an insoluble constraint as per 'insolubleIrredCt', i.e. either
    1204 
    ---        - an insoluble equality constraint (e.g. Int ~ Bool), or
    1205 
    ---        - a custom type error constraint, TypeError msg :: Constraint
    1206 
    ---   b) that does not arise from a Given or a Wanted/Wanted fundep interaction
    1200 
    +-- | Is this a definitely insoluble Wanted constraint? Namely:
    1201 
    +--
    1202 
    +--   - a Wanted,
    1203 
    +--   - which is insoluble (as per 'insolubleCt'),
    1204 
    +--   - that does not arise from a Given or a Wanted/Wanted fundep interaction.
    1205 
    +--
    1207 1206 
     -- See Note [Insoluble Wanteds]
    1208 1207 
     insolubleWantedCt ct
    1209 
    -  | CIrredCan ir_ct <- ct
    1210 
    -      -- CIrredCan: see (IW1) in Note [Insoluble Wanteds]
    1211 
    -  , IrredCt { ir_ev = ev } <- ir_ct
    1212 
    -  , CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rewriters })  <- ev
    1208 
    +  | CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rewriters })
    1209 
    +      <- ctEvidence ct
    1213 1210 
           -- It's a Wanted
    1214 
    -  , insolubleIrredCt ir_ct
    1211 
    +  , insolubleCt ct
    1215 1212 
           -- It's insoluble
    1216 1213 
       , isEmptyRewriterSet rewriters
    1217 
    -      -- It has no rewriters; see (IW2) in Note [Insoluble Wanteds]
    1214 
    +      -- It has no rewriters – see (IW1) in Note [Insoluble Wanteds]
    1218 1215 
       , not (isGivenLoc loc)
    1219 
    -      -- isGivenLoc: see (IW3) in Note [Insoluble Wanteds]
    1216 
    +      -- It doesn't arise from a Given – see (IW2) in Note [Insoluble Wanteds]
    1220 1217 
       , not (isWantedWantedFunDepOrigin (ctLocOrigin loc))
    1221 
    -      -- origin check: see (IW4) in Note [Insoluble Wanteds]
    1218 
    +      -- It doesn't arise from a W/W fundep interaction – see (IW3) in Note [Insoluble Wanteds]
    1222 1219 
       = True
    1223 1220
    1224 1221 
       | otherwise
    1225 1222 
       = False
    1226 1223
    1227 
    --- | Returns True of constraints that are definitely insoluble,
    1228 
    ---   as well as TypeError constraints.
    1229 
    --- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
    1224 
    +-- | Returns True of constraints that are definitely insoluble, including
    1225 
    +-- constraints that include custom type errors, as per (1)
    1226 
    +-- in Note [Custom type errors in constraints].
    1230 1227 
     --
    1231 
    --- The function is tuned for application /after/ constraint solving
    1232 
    ---       i.e. assuming canonicalisation has been done
    1233 
    --- That's why it looks only for IrredCt; all insoluble constraints
    1234 
    --- are put into CIrredCan
    1228 
    +-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
    1235 1229 
     insolubleCt :: Ct -> Bool
    1236 
    -insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
    1237 
    -insolubleCt _                 = False
    1238 
    -
    1239 
    -insolubleIrredCt :: IrredCt -> Bool
    1240 
    --- Returns True of Irred constraints that are /definitely/ insoluble
    1241 
    ---
    1242 
    --- This function is critical for accurate pattern-match overlap warnings.
    1243 
    --- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver
    1244 
    ---
    1245 
    --- Note that this does not traverse through the constraint to find
    1246 
    --- nested custom type errors: it only detects @TypeError msg :: Constraint@,
    1247 
    --- and not e.g. @Eq (TypeError msg)@.
    1248 
    -insolubleIrredCt (IrredCt { ir_ev = ev, ir_reason = reason })
    1249 
    -  =  isInsolubleReason reason
    1250 
    -  || isTopLevelUserTypeError (ctEvPred ev)
    1251 
    -  -- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg"
    1252 
    -  -- and "Unsatisfiable msg". It deliberately does not detect TypeError
    1253 
    -  -- nested in a type (e.g. it does not use "containsUserTypeError"), as that
    1254 
    -  -- would be too eager: the TypeError might appear inside a type family
    1255 
    -  -- application which might later reduce, but we only want to return 'True'
    1256 
    -  -- for constraints that are definitely insoluble.
    1257 
    -  --
    1258 
    -  -- For example: Num (F Int (TypeError "msg")), where F is a type family.
    1259 
    -  --
    1260 
    -  -- Test case: T11503, with the 'Assert' type family:
    1261 
    -  --
    1262 
    -  -- > type Assert :: Bool -> Constraint -> Constraint
    1263 
    -  -- > type family Assert check errMsg where
    1264 
    -  -- >   Assert 'True  _errMsg = ()
    1265 
    -  -- >   Assert _check errMsg  = errMsg
    1230 
    +insolubleCt ct
    1231 
    +  | CIrredCan (IrredCt { ir_reason = reason }) <- ct
    1232 
    +  , isInsolubleReason reason
    1233 
    +  = True
    1234 
    +  | isJust $ isUnsatisfiableCt_maybe pred
    1235 
    +  = True
    1236 
    +  | containsUserTypeError False pred
    1237 
    +      -- False <=> do not look under ty-fam apps, AppTy etc.
    1238 
    +      -- See (UTE1) in Note [Custom type errors in constraints].
    1239 
    +  = True
    1240 
    +  | otherwise
    1241 
    +  = False
    1242 
    +  where
    1243 
    +    pred = ctPred ct
    1266 1244
    1267 1245 
     -- | Does this hole represent an "out of scope" error?
    1246 
    +--
    1268 1247 
     -- See Note [Insoluble holes]
    1269 1248 
     isOutOfScopeHole :: Hole -> Bool
    1270 1249 
     isOutOfScopeHole (Hole { hole_occ = occ }) = not (startsWithUnderscore (occName occ))
    ... ... @@ -1312,12 +1291,7 @@ Note [Insoluble Wanteds]
    1312 1291 
     insolubleWantedCt returns True of a Wanted constraint that definitely
    1313 1292 
     can't be solved.  But not quite all such constraints; see wrinkles.
    1314 1293
    1315 
    -(IW1) insolubleWantedCt is tuned for application /after/ constraint
    1316 
    -   solving i.e. assuming canonicalisation has been done.  That's why
    1317 
    -   it looks only for IrredCt; all insoluble constraints are put into
    1318 
    -   CIrredCan
    1319 
    -
    1320 
    -(IW2) We only treat it as insoluble if it has an empty rewriter set.  (See Note
    1294 
    +(IW1) We only treat it as insoluble if it has an empty rewriter set.  (See Note
    1321 1295 
        [Wanteds rewrite Wanteds].)  Otherwise #25325 happens: a Wanted constraint A
    1322 1296 
        that is /not/ insoluble rewrites some other Wanted constraint B, so B has A
    1323 1297 
        in its rewriter set.  Now B looks insoluble.  The danger is that we'll
    ... ... @@ -1325,10 +1299,10 @@ can't be solved. But not quite all such constraints; see wrinkles.
    1325 1299 
        reporting A because there is an insoluble B lying around.  (This suppression
    1326 1300 
        happens in GHC.Tc.Errors.mkErrorItem.)  Solution: don't treat B as insoluble.
    1327 1301
    1328 
    -(IW3) If the Wanted arises from a Given (how can that happen?), don't
    1302 
    +(IW2) If the Wanted arises from a Given (how can that happen?), don't
    1329 1303 
        treat it as a Wanted insoluble (obviously).
    1330 1304
    1331 
    -(IW4) If the Wanted came from a  Wanted/Wanted fundep interaction, don't
    1305 
    +(IW3) If the Wanted came from a Wanted/Wanted fundep interaction, don't
    1332 1306 
        treat the constraint as insoluble. See Note [Suppressing confusing errors]
    1333 1307 
        in GHC.Tc.Errors
    1334 1308
    ... ... @@ -1354,71 +1328,165 @@ Yuk!
    1354 1328
    1355 1329 
     {- Note [Custom type errors in constraints]
    1356 1330 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1357 
    -When GHC reports a type-error about an unsolved-constraint, we check
    1358 
    -to see if the constraint contains any custom-type errors, and if so
    1359 
    -we report them.  Here are some examples of constraints containing type
    1360 
    -errors:
    1361 
    -
    1362 
    -  TypeError msg           -- The actual constraint is a type error
    1363 
    -
    1364 
    -  TypError msg ~ Int      -- Some type was supposed to be Int, but ended up
    1365 
    -                          -- being a type error instead
    1366 
    -
    1367 
    -  Eq (TypeError msg)      -- A class constraint is stuck due to a type error
    1368 
    -
    1369 
    -  F (TypeError msg) ~ a   -- A type function failed to evaluate due to a type err
    1370 
    -
    1371 
    -It is also possible to have constraints where the type error is nested deeper,
    1372 
    -for example see #11990, and also:
    1373 
    -
    1374 
    -  Eq (F (TypeError msg))  -- Here the type error is nested under a type-function
    1375 
    -                          -- call, which failed to evaluate because of it,
    1376 
    -                          -- and so the `Eq` constraint was unsolved.
    1377 
    -                          -- This may happen when one function calls another
    1378 
    -                          -- and the called function produced a custom type error.
    1379 
    -
    1380 
    -A good use-case is described in "Detecting the undetectable"
    1381 
    -   https://blog.csongor.co.uk/report-stuck-families/
    1382 
    -which features
    1383 
    -   type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where
    1384 
    -     Assert _ Dummy _ = Any
    1385 
    -     Assert _ _ k = k
    1386 
    -and an unsolved constraint like
    1387 
    -   Assert (TypeError ...) (F ty1) ty1 ~ ty2
    1388 
    -that reports that (F ty1) remains stuck.
    1331 
    +A custom type error is a type family application 'TypeError msg' where
    1332 
    +'msg :: ErrorMessage', or an Unsatisfiable constraint.
    1333 
    +See Note [Custom type errors] and Note [The Unsatisfiable constraint]
    1334 
    +in GHC.Internal.TypeError.
    1335 
    +
    1336 
    +There are two ways in which the presence of such custom type errors inside a
    1337 
    +type impact GHC's behaviour:
    1338 
    +
    1339 
    +  (UTE1)
    1340 
    +    Constraints that contain a custom type error are considered to be
    1341 
    +    insoluble. This affects pattern-match warnings, as explained in
    1342 
    +    Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
    1343 
    +
    1344 
    +    This includes examples such as:
    1345 
    +
    1346 
    +      TypeError msg           -- The actual constraint is a type error
    1347 
    +
    1348 
    +      TypeError msg ~# Int    -- Some type was supposed to be Int, but ended up
    1349 
    +                              -- being a type error instead
    1350 
    +
    1351 
    +    However, we must be careful about occurrences of custom type errors
    1352 
    +    nested inside the constraint, as they may not make the constraint
    1353 
    +    insoluble. This is explained in Note [When is a constraint insoluble?]
    1354 
    +    in GHC.Tc.Solver. In particular:
    1355 
    +
    1356 
    +      a. Do not look inside type family applications.
    1357 
    +      b. Do not look inside class constraints.
    1358 
    +      c. Do not look inside AppTy or in arguments of a type family past its arity.
    1359 
    +      d. Only consider 'TypeError msg ~ rhs' to be insoluble if rhs definitely
    1360 
    +         cannot unify with 'TypeError msg', e.g. if 'rhs = Int' the constraint
    1361 
    +         is insoluble, but if 'rhs = k[sk]' then it isn't.
    1362 
    +
    1363 
    +    These subtle cases are tested in T26400b.
    1364 
    +
    1365 
    +    A good use-case for type errors nested under type family applications is
    1366 
    +    described in "Detecting the undetectable" (https://blog.csongor.co.uk/report-stuck-families/)
    1367 
    +    which features:
    1368 
    +       type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where
    1369 
    +         Assert _ Dummy _ = Any
    1370 
    +         Assert _ _ k = k
    1371 
    +    and an unsolved constraint like 'Assert (TypeError ...) (F ty1) ty1 ~ ty2'
    1372 
    +    which reports when (F ty1) remains stuck.
    1373 
    +
    1374 
    +  (UTE2)
    1375 
    +    When reporting unsolved constraints, we pull out any custom type errors
    1376 
    +    and report the corresponding message to the user.
    1377 
    +
    1378 
    +    Unlike in (UTE1), we do want to pull out 'TypeError' wherever it occurs
    1379 
    +    inside the type, including inside type-family applications. We tried to
    1380 
    +    solve the constraint, reduce type families etc, but the constraint
    1381 
    +    remained unsolved all the way till the end. Now that we are reporting the
    1382 
    +    error, it makes sense to pull out the 'TypeError' and report the custom
    1383 
    +    error message to the user, as the intention is that this message might
    1384 
    +    be informative.
    1385 
    +
    1386 
    +    Examples:
    1387 
    +
    1388 
    +      Num (TypeError msg)     -- A class constraint is stuck due to a type error
    1389 
    +
    1390 
    +      F (TypeError msg) ~ a   -- A type function failed to evaluate due to a type error
    1391 
    +
    1392 
    +      Eq (F (TypeError msg))  -- Here the type error is nested under a type-function
    1393 
    +                              -- call, which failed to evaluate because of it,
    1394 
    +                              -- and so the `Eq` constraint was unsolved.
    1395 
    +                              -- This may happen when one function calls another
    1396 
    +                              -- and the called function produced a custom type error.
    1397 
    +
    1398 
    +We use a single function, 'userTypeError_maybe', to pull out TypeError according
    1399 
    +to the rules of either (UTE1) or (UTE2), depending on the passed in boolean
    1400 
    +flag to 'userTypeError_maybe': 'False' for (UTE1) and 'True' for (UTE2).
    1389 1401 
     -}
    1390 1402
    1391 
    --- | A constraint is considered to be a custom type error, if it contains
    1392 
    --- custom type errors anywhere in it.
    1393 
    --- See Note [Custom type errors in constraints]
    1394 
    -getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType
    1395 
    -getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred
    1396 
    -                                  : map getUserTypeErrorMsg (subTys pred)
    1403 
    +-- | Does this type contain 'TypeError msg', either at the top-level or
    1404 
    +-- nested within it somewhere?
    1405 
    +--
    1406 
    +-- If so, return the error message.
    1407 
    +--
    1408 
    +-- See Note [Custom type errors in constraints].
    1409 
    +userTypeError_maybe
    1410 
    +  :: Bool -- ^ Look everywhere: inside type-family applications, class constraints, AppTys etc?
    1411 
    +  -> Type
    1412 
    +  -> Maybe ErrorMsgType
    1413 
    +userTypeError_maybe look_everywhere = go
    1397 1414 
       where
    1398 
    -   -- Richard thinks this function is very broken. What is subTys
    1399 
    -   -- supposed to be doing? Why are exactly-saturated tyconapps special?
    1400 
    -   -- What stops this from accidentally ripping apart a call to TypeError?
    1401 
    -    subTys t = case splitAppTys t of
    1402 
    -                 (t,[]) ->
    1403 
    -                   case splitTyConApp_maybe t of
    1404 
    -                              Nothing     -> []
    1405 
    -                              Just (_,ts) -> ts
    1406 
    -                 (t,ts) -> t : ts
    1407 
    -
    1408 
    --- | Is this an user error message type, i.e. either the form @TypeError err@ or
    1409 
    --- @Unsatisfiable err@?
    1410 
    -isTopLevelUserTypeError :: PredType -> Bool
    1411 
    -isTopLevelUserTypeError pred =
    1412 
    -  isJust (userTypeError_maybe pred) || isJust (isUnsatisfiableCt_maybe pred)
    1415 
    +    go ty
    1416 
    +      | Just ty' <- coreView ty
    1417 
    +      = go ty'
    1418 
    +    go (TyConApp tc tys)
    1419 
    +      | tyConName tc == errorMessageTypeErrorFamName
    1420 
    +      , _kind : msg : _ <- tys
    1421 
    +              -- There may be more than 2 arguments, if the type error is
    1422 
    +              -- used as a type constructor (e.g. at kind `Type -> Type`).
    1423 
    +      = Just msg
    1424 
    +
    1425 
    +      -- (UTE1.d) TypeError msg ~ a is only insoluble if 'a' cannot be a type error
    1426 
    +      | not look_everywhere
    1427 
    +      , tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
    1428 
    +      , [ ki1, ki2, ty1, ty2 ] <- tys
    1429 
    +      = if | Just msg <- go ki1
    1430 
    +           , isRigidTy ki2
    1431 
    +           -> Just msg
    1432 
    +           | Just msg <- go ki2
    1433 
    +           , isRigidTy ki1
    1434 
    +           -> Just msg
    1435 
    +           | Just msg <- go ty1
    1436 
    +           , isRigidTy ty2
    1437 
    +           -> Just msg
    1438 
    +           | Just msg <- go ty2
    1439 
    +           , isRigidTy ty1
    1440 
    +           -> Just msg
    1441 
    +           | otherwise
    1442 
    +           -> Nothing
    1443 
    +
    1444 
    +      -- (UTE1.a) Don't look under type family applications.
    1445 
    +      | tyConMustBeSaturated tc
    1446 
    +      , not look_everywhere
    1447 
    +      = Nothing
    1448 
    +        -- (UTE1.c) Don't even look in the arguments past the arity of the TyCon.
    1449 
    +
    1450 
    +      -- (UTE1.b) Don't look inside class constraints.
    1451 
    +      | isClassTyCon tc
    1452 
    +      , not look_everywhere
    1453 
    +      = foldr (firstJust . go) Nothing (drop (tyConArity tc) tys)
    1454 
    +      | otherwise
    1455 
    +      = foldr (firstJust . go) Nothing tys
    1456 
    +    go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `firstJust` go ty
    1457 
    +    go (FunTy { ft_mult = mult, ft_arg = arg, ft_res = res })
    1458 
    +      = firstJusts
    1459 
    +          [ go mult
    1460 
    +          , go (typeKind arg)
    1461 
    +          , go (typeKind res)
    1462 
    +          , go arg
    1463 
    +          , go res ]
    1464 
    +    go (AppTy t1 t2)
    1465 
    +      -- (UTE1.c) Don't look inside AppTy.
    1466 
    +      | not look_everywhere
    1467 
    +      = Nothing
    1468 
    +      | otherwise
    1469 
    +      = go t1 `firstJust` go t2
    1470 
    +    go (CastTy ty _co) = go ty
    1471 
    +    go (TyVarTy tv) = go (tyVarKind tv)
    1472 
    +    go (CoercionTy {}) = Nothing
    1473 
    +    go (LitTy {}) = Nothing
    1413 1474
    1414 1475 
     -- | Does this constraint contain an user error message?
    1415 1476 
     --
    1416 1477 
     -- That is, the type is either of the form @Unsatisfiable err@, or it contains
    1417 1478 
     -- a type of the form @TypeError msg@, either at the top level or nested inside
    1418 1479 
     -- the type.
    1419 
    -containsUserTypeError :: PredType -> Bool
    1420 
    -containsUserTypeError pred =
    1421 
    -  isJust (getUserTypeErrorMsg pred) || isJust (isUnsatisfiableCt_maybe pred)
    1480 
    +--
    1481 
    +-- See Note [Custom type errors in constraints].
    1482 
    +containsUserTypeError
    1483 
    +  :: Bool -- ^ look inside type-family applications, 'AppTy', etc?
    1484 
    +  -> PredType
    1485 
    +  -> Bool
    1486 
    +containsUserTypeError look_in_famapps pred =
    1487 
    +  isJust (isUnsatisfiableCt_maybe pred)
    1488 
    +    ||
    1489 
    +  isJust (userTypeError_maybe look_in_famapps pred)
    1422 1490
    1423 1491 
     -- | Is this type an unsatisfiable constraint?
    1424 1492 
     -- If so, return the error message.

  • compiler/GHC/Tc/Validity.hs
    ... ... @@ -31,6 +31,7 @@ import GHC.Tc.Instance.Family
    31 31 
     import GHC.Tc.Types.Origin
    32 32 
     import GHC.Tc.Types.Rank
    33 33 
     import GHC.Tc.Errors.Types
    34 
    +import GHC.Tc.Types.Constraint ( userTypeError_maybe )
    34 35 
     import GHC.Tc.Utils.Env (tcLookupId)
    35 36 
     import GHC.Tc.Utils.TcType
    36 37 
     import GHC.Tc.Utils.Monad
    ... ... @@ -282,7 +283,12 @@ checkUserTypeError ctxt ty
    282 283 
       | TySynCtxt {} <- ctxt  -- Do not complain about TypeError on the
    283 284 
       = return ()             -- RHS of type synonyms. See #20181
    284 285
    285 
    -  | Just msg <- deepUserTypeError_maybe ty
    286 
    +  | Just msg <- userTypeError_maybe False ty
    287 
    +      --                            ^^^^^
    288 
    +      -- Don't look under type-family applications! We only want to pull out
    289 
    +      -- definite errors.
    290 
    +      --
    291 
    +      -- See (UTE1) in Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint.
    286 292 
       = do { env0 <- liftZonkM tcInitTidyEnv
    287 293 
            ; let (env1, tidy_msg) = tidyOpenTypeX env0 msg
    288 294 
            ; failWithTcM (env1, TcRnUserTypeError tidy_msg) }

  • testsuite/tests/pmcheck/should_compile/T26400.hs
    1 
    +{-# LANGUAGE DataKinds #-}
    2 
    +{-# LANGUAGE GADTs #-}
    3 
    +{-# LANGUAGE StandaloneKindSignatures #-}
    4 
    +{-# LANGUAGE TypeFamilies #-}
    5 
    +{-# LANGUAGE UnliftedDatatypes #-}
    6 
    +
    7 
    +module T26400 where
    8 
    +
    9 
    +import GHC.Exts ( UnliftedType )
    10 
    +import GHC.TypeLits ( TypeError, ErrorMessage(..) )
    11 
    +
    12 
    +data N = Z | S N
    13 
    +
    14 
    +-- Make this type unlifted to avoid any subtleties about laziness
    15 
    +type SNat :: N -> UnliftedType
    16 
    +data SNat n where
    17 
    +  SZ :: SNat Z
    18 
    +  SS :: SNat n -> SNat (S n)
    19 
    +
    20 
    +type (-) :: N -> N -> N
    21 
    +type family a - b where
    22 
    +  n   - Z   = n
    23 
    +  Z   - S _ = TypeError ( Text "impossible" )
    24 
    +  S n - S m = n - m
    25 
    +
    26 
    +testFn :: SNat n -> SNat m -> SNat (n - m) -> Int
    27 
    +testFn SZ (SS _) SZ     = 666
    28 
    +testFn SZ (SS _) (SS _) = 999
    29 
    +  -- [G] g1 :: n ~ Z
    30 
    +  -- [G] g2 :: m ~ S m1
    31 
    +  -- [G] g3 :: (n-m) ~ S m2
    32 
    +  -- Use the first two givens to substitute in the third, we get:
    33 
    +  -- [G] g3' :: Z - S m1 ~ S m2
    34 
    +  -- Reduce the LHS using the type family
    35 
    +  -- [G] g3'' :: TypeError ... ~ S m2
    36 
    +  -- Hence g3'' is insoluble and the equation can never match
    37 
    +testFn _ _ _ = 1

  • testsuite/tests/pmcheck/should_compile/T26400.stderr
    1 
    +T26400.hs:27:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
    2 
    +    Pattern match is redundant
    3 
    +    In an equation for ‘testFn’: testFn SZ (SS _) SZ = ...
    4 
    +
    5 
    +T26400.hs:28:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
    6 
    +    Pattern match is redundant
    7 
    +    In an equation for ‘testFn’: testFn SZ (SS _) (SS _) = ...
    8 
    +

  • testsuite/tests/pmcheck/should_compile/T26400b.hs
    1 
    +{-# LANGUAGE DataKinds #-}
    2 
    +{-# LANGUAGE GADTs #-}
    3 
    +{-# LANGUAGE StandaloneKindSignatures #-}
    4 
    +{-# LANGUAGE TypeFamilies #-}
    5 
    +
    6 
    +module T26400b where
    7 
    +
    8 
    +import Data.Kind
    9 
    +import GHC.TypeLits ( TypeError, ErrorMessage(..) )
    10 
    +
    11 
    +type F :: Type -> Type -> Type
    12 
    +type family F a b where
    13 
    +  F Float _ = Bool
    14 
    +  F _     a = a
    15 
    +
    16 
    +type C :: Type -> Type -> Constraint
    17 
    +class C a b
    18 
    +instance C () b
    19 
    +
    20 
    +type Boom :: Type -> Type
    21 
    +type family Boom a where
    22 
    +  Boom () = TypeError (Text "boom")
    23 
    +
    24 
    +type TF :: Type -> ( Type -> Type -> Constraint )
    25 
    +type family TF a where
    26 
    +  TF () = C
    27 
    +
    28 
    +type G :: Type -> Type -> Type
    29 
    +data G a b where
    30 
    +  G1 :: a -> F b (Boom a) -> G a b
    31 
    +  G2 :: C a (Boom a) => a -> G a b
    32 
    +  G3 :: (TF b) a (Boom a) => a -> G a b
    33 
    +  G4 :: (b ~ Boom a) => G a b
    34 
    +
    35 
    +g :: G () b -> Int
    36 
    +g (G1 {}) = 1 -- not redundant: F b (TypeError ...) can be solved if F reduces
    37 
    +g (G2 {}) = 2 -- not redundant: C () (TypeError ...) is not insoluble
    38 
    +g (G3 {}) = 3 -- not redundant: TF b () (TypeError ...) could reduce to C () (TypeError ...)
    39 
    +g (G4 {}) = 4 -- not redundant: b ~ TypeError ... could be solved depending on instantiation of b

  • testsuite/tests/pmcheck/should_compile/all.T
    ... ... @@ -123,6 +123,8 @@ test('T21761', [], compile, [overlapping_incomplete])
    123 123 
     test('T22964', [], compile, [overlapping_incomplete])
    124 124 
     test('T23445', [], compile, [overlapping_incomplete])
    125 125 
     test('T24234', [], compile, [overlapping_incomplete+'-Wincomplete-uni-patterns'])
    126 
    +test('T26400', [], compile, [overlapping_incomplete])
    127 
    +test('T26400b', [], compile, [overlapping_incomplete])
    126 128
    127 129 
     # Series (inspired) by Luke Maranget
    128 130

  • testsuite/tests/typecheck/should_fail/T20241b.stderr
    1 
    -
    2 1 
     T20241b.hs:16:8: error: [GHC-47403]
    3 2 
         • Boom
    4 3 
         • In the type signature:
    ... ... @@ -6,11 +5,14 @@ T20241b.hs:16:8: error: [GHC-47403]
    6 5 
                                                 -> Type -> Constraint) IO) a =>
    7 6 
                    Proxy a -> ()
    8 7
    9 
    -T20241b.hs:20:8: error: [GHC-47403]
    8 
    +T20241b.hs:20:8: error: [GHC-64725]
    10 9 
         • Boom
    11 
    -    • In the type signature:
    10 
    +    • In the ambiguity check for ‘bar’
    11 
    +      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    12 
    +      In the type signature:
    12 13 
             bar :: ((c :: Constraint
    13 14 
                           -> Type -> Constraint) (((TypeError (Text "Boom") :: (Type -> Type)
    14 15 
                                                                                -> Type
    15 16 
                                                                                   -> Constraint) IO) a)) a =>
    16 17 
                    Proxy a -> ()
    18 
    +

  • testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
    ... ... @@ -9,11 +9,11 @@ UnliftedNewtypesFamilyKindFail2.hs:12:20: error: [GHC-83865]
    9 9 
         • In the first argument of ‘F’, namely ‘5’
    10 10 
           In the newtype family instance declaration for ‘F’
    11 11
    12 
    -UnliftedNewtypesFamilyKindFail2.hs:12:31: [GHC-83865]
    13 
    -     Expected a type,
    12 
    +UnliftedNewtypesFamilyKindFail2.hs:12:31: error: [GHC-83865]
    13 
    +    • Expected a type,
    14 14 
           but ‘5’ has kind
    15 15 
           ‘GHC.Internal.Bignum.Natural.Natural’
    16 
    -     In the first argument of ‘F’, namely ‘5’
    16 
    +    • In the first argument of ‘F’, namely ‘5’
    17 17 
           In the type ‘(F 5)’
    18 18 
           In the definition of data constructor ‘MkF’
    19 19

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help