Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC

Commits:

14 changed files:

Changes:

  • compiler/GHC/Tc/Errors.hs
    ... ... @@ -1509,11 +1509,12 @@ coercion.
    1509 1509 
     mkIrredErr :: SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport
    1510 1510 
     mkIrredErr ctxt items
    1511 1511 
       = do { (ctxt, binds, item1) <- relevantBindings True ctxt item1
    1512 
    -       ; couldNotDeduceErr <- mkCouldNotDeduceErr (getUserGivens ctxt) (item1 :| others) Nothing
    1512 
    +       ; couldNotDeduceErr <- mkCouldNotDeduceErr useful_givens (item1 :| others) Nothing
    1513 1513 
            ; let msg = important ctxt $ mkPlainMismatchMsg couldNotDeduceErr
    1514 1514 
            ; return $ add_relevant_bindings binds msg  }
    1515 1515 
       where
    1516 1516 
         item1:|others = tryFilter (not . ei_suppress) items
    1517 
    +    useful_givens = getUsefulGivens ctxt item1
    1517 1518
    1518 1519 
     {- Note [Constructing Hole Errors]
    1519 1520 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -1694,8 +1695,8 @@ validHoleFits ctxt@(CEC { cec_encl = implics
    1694 1695 
     givenConstraints :: SolverReportErrCtxt -> [(Type, RealSrcSpan)]
    1695 1696 
     -- Returned outermost first
    1696 1697 
     -- See Note [Constraints include ...]
    1697 
    -givenConstraints ctxt
    1698 
    -  = do { implic@Implic{ ic_given = given } <- getUserGivens ctxt
    1698 
    +givenConstraints (CEC { cec_encl = implics })
    1699 
    +  = do { implic@Implic{ ic_given = given } <- getGivensFromImplics implics
    1699 1700 
            ; constraint <- given
    1700 1701 
            ; return (varType constraint, getCtLocEnvLoc (ic_env implic)) }
    1701 1702
    ... ... @@ -2105,6 +2106,7 @@ eqInfoMsgs ty1 ty2
    2105 2106
    2106 2107 
     misMatchOrCND :: SolverReportErrCtxt -> ErrorItem
    2107 2108 
                   -> TcType -> TcType -> TcM MismatchMsg
    2109 
    +-- Make a message for a failed equality constraint (t1 ~ t2)
    2108 2110 
     -- If oriented then ty1 is actual, ty2 is expected
    2109 2111 
     misMatchOrCND ctxt item ty1 ty2
    2110 2112 
       | ei_insoluble item   -- See Note [Insoluble mis-match]
    ... ... @@ -2120,7 +2122,8 @@ misMatchOrCND ctxt item ty1 ty2
    2120 2122
    2121 2123 
       where
    2122 2124 
         level   = ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
    2123 
    -    givens  = [ given | given <- getUserGivens ctxt, ic_given_eqs given /= NoGivenEqs ]
    2125 
    +    givens  = [ given | given <- getUsefulGivens ctxt item
    2126 
    +                      , ic_given_eqs given /= NoGivenEqs ]
    2124 2127 
                   -- Keep only UserGivens that have some equalities.
    2125 2128 
                   -- See Note [Suppress redundant givens during error reporting]
    2126 2129
    ... ... @@ -2302,7 +2305,8 @@ mkQCErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM
    2302 2305 
     mkQCErr ctxt items
    2303 2306 
       | item1 :| _ <- tryFilter (not . ei_suppress) items
    2304 2307 
         -- Ignore multiple qc-errors on the same line
    2305 
    -  = do { couldNotDeduceErr <- mkCouldNotDeduceErr (getUserGivens ctxt) (item1 :| []) Nothing
    2308 
    +  = do { couldNotDeduceErr <- mkCouldNotDeduceErr (getUsefulGivens ctxt item1)
    2309 
    +                                                  (item1 :| []) Nothing
    2306 2310 
            ; return $ important ctxt $ mkPlainMismatchMsg couldNotDeduceErr }
    2307 2311
    2308 2312
    ... ... @@ -2332,7 +2336,8 @@ mkDictErr ctxt orig_items@(item1 :| others)
    2332 2336 
       where
    2333 2337 
         items = tryFilter (not . ei_suppress) orig_items
    2334 2338
    2335 
    -    no_givens = null (getUserGivens ctxt)
    2339 
    +    useful_givens = getUsefulGivens ctxt item1
    2340 
    +    no_givens = null useful_givens
    2336 2341
    2337 2342 
         is_no_inst (item, (matches, unifiers, _))
    2338 2343 
           =  no_givens
    ... ... @@ -2471,9 +2476,9 @@ mkCouldNotDeduceErr
    2471 2476 
       -> NonEmpty ErrorItem
    2472 2477 
       -> Maybe CND_ExpectedActual
    2473 2478 
       -> TcM MismatchMsg
    2474 
    -mkCouldNotDeduceErr user_givens items@(item :| _) mb_ea
    2479 
    +mkCouldNotDeduceErr useful_givens items@(item :| _) mb_ea
    2475 2480 
       = do { mb_noBuiltinInst_info <- getNoBuiltinInstMsg item
    2476 
    -       ; return $ CouldNotDeduce user_givens items mb_ea mb_noBuiltinInst_info }
    2481 
    +       ; return $ CouldNotDeduce useful_givens items mb_ea mb_noBuiltinInst_info }
    2477 2482
    2478 2483 
     getNoBuiltinInstMsg :: ErrorItem -> TcM (Maybe NoBuiltinInstanceMsg)
    2479 2484 
     getNoBuiltinInstMsg item =

  • compiler/GHC/Tc/Errors/Ppr.hs
    ... ... @@ -4178,7 +4178,7 @@ pprTcSolverReportMsg _ (ExpectingMoreArguments n thing) =
    4178 4178 
          | n == 1    = text "more argument to"
    4179 4179 
          | otherwise = text "more arguments to" -- n > 1
    4180 4180 
     pprTcSolverReportMsg ctxt (UnboundImplicitParams (item :| items)) =
    4181 
    -  let givens = getUserGivens ctxt
    4181 
    +  let givens = getUsefulGivens ctxt item
    4182 4182 
       in if null givens
    4183 4183 
          then addArising (errorItemCtLoc item) $
    4184 4184 
                 sep [ text "Unbound implicit parameter" <> plural preds
    ... ... @@ -4233,7 +4233,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
    4233 4233 
         (ambig_kvs, ambig_tvs) = ambigTkvsOfTy pred
    4234 4234 
         ambigs = ambig_kvs ++ ambig_tvs
    4235 4235 
         has_ambigs = not (null ambigs)
    4236 
    -    useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
    4236 
    +    useful_givens = getUsefulGivens ctxt item
    4237 4237 
              -- useful_givens are the enclosing implications with non-empty givens,
    4238 4238 
              -- modulo the horrid discardProvCtxtGivens
    4239 4239 
         lead_with_ambig = not (null ambigs)
    ... ... @@ -4298,7 +4298,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
    4298 4298 
           = empty
    4299 4299
    4300 4300 
         ----------- Possible fixes ----------------
    4301 
    -    ctxt_fixes = ctxtFixes has_ambigs pred implics
    4301 
    +    ctxt_fixes = ctxtFixes ctxt has_ambigs pred
    4302 4302
    4303 4303 
         drv_fixes = case orig of
    4304 4304 
                        DerivOrigin standalone             -> [drv_fix standalone]
    ... ... @@ -4332,7 +4332,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
    4332 4332 
                                  Just (_, tys) -> not (all isTyVarTy tys)
    4333 4333 
                                  Nothing       -> False
    4334 4334
    4335 
    -pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item matches unifiers) =
    4335 
    +pprTcSolverReportMsg ctxt (OverlappingInstances item matches unifiers) =
    4336 4336 
       vcat
    4337 4337 
         [ addArising ct_loc $
    4338 4338 
             (text "Overlapping instances for"
    ... ... @@ -4375,7 +4375,7 @@ pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item match
    4375 4375 
         (clas, tys)     = getClassPredTys pred
    4376 4376 
         tyCoVars        = tyCoVarsOfTypesList tys
    4377 4377 
         famTyCons       = filter isFamilyTyCon $ concatMap (nonDetEltsUniqSet . tyConsOfType) tys
    4378 
    -    useful_givens   = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
    4378 
    +    useful_givens   = getUsefulGivens ctxt item
    4379 4379 
         matching_givens = mapMaybe matchable useful_givens
    4380 4380 
         matchable implic@(Implic { ic_given = evvars, ic_info = skol_info })
    4381 4381 
           = case ev_vars_matching of
    ... ... @@ -4707,10 +4707,13 @@ pprMismatchMsg ctxt
    4707 4707 
           | otherwise          = vcat ( addArising ct_loc no_deduce_msg
    4708 4708 
                                       : pp_from_givens useful_givens)
    4709 4709
    4710 
    -    ea_supplementary = case mb_ea of
    4711 
    -      Nothing -> empty
    4712 
    -      Just (CND_ExpectedActual level ty1 ty2) ->
    4713 
    -        mk_supplementary_ea_msg ctxt level ty1 ty2 orig
    4710 
    +    ea_supplementary
    4711 
    +      | Just (CND_ExpectedActual level ty1 ty2) <- mb_ea
    4712 
    +      = mk_supplementary_ea_msg ctxt level ty1 ty2 orig
    4713 
    +      | Just InsolubleFunDepReason <- ei_m_reason item
    4714 
    +      = text "The functional dependencies arising from this constraint are insoluble"
    4715 
    +      | otherwise
    4716 
    +      = empty
    4714 4717
    4715 4718 
         ct_loc = errorItemCtLoc item
    4716 4719 
         orig   = ctLocOrigin ct_loc
    ... ... @@ -5583,8 +5586,8 @@ show_fixes [] = empty
    5583 5586 
     show_fixes (f:fs) = sep [ text "Possible fix:"
    5584 5587 
                             , nest 2 (vcat (f : map (text "or" <+>) fs))]
    5585 5588
    5586 
    -ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
    5587 
    -ctxtFixes has_ambig_tvs pred implics
    5589 
    +ctxtFixes :: SolverReportErrCtxt -> Bool -> PredType -> [SDoc]
    5590 
    +ctxtFixes (CEC {cec_encl = implics}) has_ambig_tvs pred
    5588 5591 
       | not has_ambig_tvs
    5589 5592 
       , isTyVarClassPred pred   -- Don't suggest adding (Eq T) to the context, say
    5590 5593 
       , (skol:skols) <- usefulContext implics pred

  • compiler/GHC/Tc/Errors/Types.hs
    ... ... @@ -62,7 +62,7 @@ module GHC.Tc.Errors.Types (
    62 62 
       , SolverReport(..), SupplementaryInfo(..)
    63 63 
       , SolverReportWithCtxt(..)
    64 64 
       , SolverReportErrCtxt(..)
    65 
    -  , getUserGivens, discardProvCtxtGivens
    65 
    +  , getUsefulGivens
    66 66 
       , TcSolverReportMsg(..)
    67 67 
       , CannotUnifyVariableReason(..)
    68 68 
       , MismatchMsg(..)
    ... ... @@ -5409,10 +5409,6 @@ data SolverReportErrCtxt
    5409 5409 
                                         -- See Note [Suppressing error messages]
    5410 5410 
           }
    5411 5411
    5412 
    -getUserGivens :: SolverReportErrCtxt -> [UserGiven]
    5413 
    --- One item for each enclosing implication
    5414 
    -getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
    5415 
    -
    5416 5412 
     ----------------------------------------------------------------------------
    5417 5413 
     --
    5418 5414 
     --   ErrorItem
    ... ... @@ -5438,7 +5434,7 @@ data ErrorItem
    5438 5434 
            , ei_loc      :: CtLoc
    5439 5435 
            , ei_m_reason :: Maybe CtIrredReason  -- If this ErrorItem was made from a
    5440 5436 
                                                  -- CtIrred, this stores the reason
    5441 
    -       , ei_insoluble :: Bool   -- True if the constraint is defdinitely insoluble
    5437 
    +       , ei_insoluble :: Bool   -- True if the constraint is definitely insoluble
    5442 5438 
                                     -- Cache of `insolubleCt`
    5443 5439
    5444 5440 
            , ei_suppress  :: Bool   -- Suppress because of
    ... ... @@ -5513,6 +5509,19 @@ message (showing both problems):
    5513 5509 
     -}
    5514 5510
    5515 5511
    5512 
    +getUsefulGivens :: SolverReportErrCtxt -> ErrorItem -> [UserGiven]
    5513 
    +-- One item for each enclosing implication
    5514 
    +getUsefulGivens (CEC {cec_encl = implics}) item
    5515 
    +  | ei_insoluble item
    5516 
    +  = []  -- If the constraint is insoluble anyway, we won't try to solve it
    5517 
    +        -- from the inert Givens, so it's positively confusing to list them.
    5518 
    +        -- Otherwise we get "Can't deduce X from X".
    5519 
    +  | otherwise
    5520 
    +  = discardProvCtxtGivens orig $
    5521 
    +    getGivensFromImplics implics
    5522 
    +  where
    5523 
    +    orig = errorItemOrigin item
    5524 
    +
    5516 5525 
     discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
    5517 5526 
     discardProvCtxtGivens orig givens  -- See Note [discardProvCtxtGivens]
    5518 5527 
       | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig

  • compiler/GHC/Tc/Solver.hs
    ... ... @@ -738,14 +738,15 @@ tcCheckGivens inerts given_ids
    738 738
    739 739 
            ; mb_res <- tryM                $  -- try_to_solve may throw an exception;
    740 740 
                                               --   e.g. reduction stack overflow
    741 
    -                   discardErrs         $  -- An exception id not an error;
    741 
    +                   discardErrs         $  -- An exception is not an error;
    742 742 
                                               --   just means "not definitely unsat"
    743 743 
                        runTcSInerts inerts $
    744 744 
                        try_to_solve given_cts
    745 745
    746 746 
            -- If mb_res = Left err, solving threw an exception, e.g. reduction stack
    747 747 
            -- overflow.  So return the original incoming inerts to say "not definitely
    748 
    -       -- unsatisfiable".
    748 
    +       -- unsatisfiable".  See (CF3) in Note [Exploiting closed type families], and
    749 
    +       -- test T15753c.
    749 750 
            ; let res = case mb_res of
    750 751 
                          Right res -> res
    751 752 
                          Left {}   -> Just inerts

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -523,7 +523,7 @@ tryEqFunDeps :: EqCt -> SolverStage ()
    523 523 
     tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs
    524 524 
                                  , eq_rhs = work_rhs
    525 525 
                                  , eq_eq_rel = eq_rel })
    526 
    -  | NomEq <- eq_rel
    526 
    +  | NomEq <- eq_rel   -- Functional dependencies only work for nominal equalities
    527 527 
       , TyFamLHS fam_tc work_args <- work_lhs     -- We have F args ~N# rhs
    528 528 
       = do { eqs_for_me <- simpleStage $ getInertFamEqsFor fam_tc work_args work_rhs
    529 529 
            ; simpleStage $ traceTcS "tryEqFunDeps" (ppr work_item $$ ppr eqs_for_me)
    ... ... @@ -1071,7 +1071,12 @@ Key point: equations that are not relevant do not need to be considered for fund
    1071 1071 
          And now we are back where we started -- loop.
    1072 1072
    1073 1073 
       We solve this by bumping the `ctLocDepth` in `solveFunDeps`, and imposing
    1074 
    -  a depth bound.  See the call to `bumpReductionDepth`.
    1074 
    +  a depth bound.  See the call to `bumpReductionDepth`.  If the depth limit
    1075 
    +  is exceeded we add an error message and fail in the monad.
    1076 
    +
    1077 
    +  Take care: when we are solving-for-unsatisfiability, in the pattern match
    1078 
    +  checker, we must carefully catch this failure: see the use of `tryM` in
    1079 
    +  `tcCheckGivens`.
    1075 1080
    1076 1081 
     (CF4) If one of the fundeps generated by interacting with the local equalities is
    1077 1082 
       definitely insoluble (e.g. Int~Bool) then there is no point in continuing to

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -66,7 +66,7 @@ module GHC.Tc.Types.Constraint (
    66 66
    67 67 
             Implication(..), implicationPrototype, checkTelescopeSkol,
    68 68 
             ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
    69 
    -        UserGiven, getUserGivensFromImplics,
    69 
    +        UserGiven, getGivensFromImplics,
    70 70 
             HasGivenEqs(..), checkImplicationInvariants,
    71 71 
             EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet,
    72 72
    ... ... @@ -1637,10 +1637,10 @@ data HasGivenEqs -- See Note [HasGivenEqs]
    1637 1637
    1638 1638 
     type UserGiven = Implication
    1639 1639
    1640 
    -getUserGivensFromImplics :: [Implication] -> [UserGiven]
    1640 
    +getGivensFromImplics :: [Implication] -> [UserGiven]
    1641 1641 
     -- The argument [Implication] is innermost first;
    1642 1642 
     --   the returned [UserGiven] is outermost first
    1643 
    -getUserGivensFromImplics implics
    1643 
    +getGivensFromImplics implics
    1644 1644 
       = get [] implics
    1645 1645 
       where
    1646 1646 
         get :: [UserGiven] -> [Implication] -> [UserGiven]

  • testsuite/tests/pmcheck/should_compile/T15753c.hs
    ... ... @@ -5,6 +5,11 @@
    5 5 
     {-# LANGUAGE TypeOperators #-}
    6 6 
     {-# LANGUAGE UndecidableInstances #-}
    7 7 
     {-# OPTIONS_GHC -Wincomplete-patterns #-}
    8 
    +
    9 
    +-- NB: After fixing #22652 this program right produces warnings
    10 
    +--     because (F u1 u1 ~ Char) is unsatisfiable
    11 
    +-- But it produces too many warnings: #26685
    12 
    +
    8 13 
     module Bug where
    9 14
    10 15 
     import Data.Kind (Type)
    ... ... @@ -34,22 +39,6 @@ type family F (u1 :: ()) (u2 :: ()) :: Type where
    34 39 
     type family Case (u :: ()) :: Type where
    35 40 
       Case '() = Int
    36 41
    37 
    ----------------------------------------
    38 
    --- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is
    39 
    --- unsatisfiable, so the empty pattern match is fine
    40 
    -g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void
    41 
    -g1a r _ _ = case r of {}
    42 
    -
    43 
    -{- Why   [G] F u1 u2 ~ Char  is unsatisfiable
    44 
    -
    45 
    -[G] F u1 u2 ~ Char =>rewrite   [G] If (IsUnit u1) (Case u2) Int ~ Char
    46 
    -                   =>(fundep)  [W] IsUnit u1 ~ True
    47 
    -                               [W] Case u2 ~ Char   <<--  insoluble: no relevant eqns
    48 
    --}
    49 
    -
    50 
    ----------------------------------------
    51 
    --- This older test matches on Refl (which is unsatisfiable)
    52 
    --- but we now get complaints from inside
    53 42 
     g1 :: F u1 u2 :~: Char
    54 43 
        -> SUnit u1 -> SUnit u2
    55 44 
        -> Void
    ... ... @@ -57,8 +46,6 @@ g1 Refl su1 su2
    57 46 
       | STrue <- sIsUnit su1
    58 47 
       = case su2 of {}
    59 48
    60 
    -
    61 
    -
    62 49 
     g2 :: F u1 u2 :~: Char
    63 50 
        -> SUnit u1 -> SUnit u2
    64 51 
        -> Void

  • testsuite/tests/pmcheck/should_compile/T15753c.stderr
    1 
    +T15753c.hs:46:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
    2 
    +    Pattern match has inaccessible right hand side
    3 
    +    In an equation for ‘g1’:
    4 
    +        g1 Refl su1 su2 | STrue <- sIsUnit su1 = ...
    5 
    +
    6 
    +T15753c.hs:47:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    7 
    +    Pattern match(es) are non-exhaustive
    8 
    +    In a case alternative:
    9 
    +        Patterns of type ‘SUnit u2’ not matched: SUnit
    10 
    +
    11 
    +T15753c.hs:52:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
    12 
    +    Pattern match has inaccessible right hand side
    13 
    +    In an equation for ‘g2’: g2 Refl su1 su2 = ...
    14 
    +
    15 
    +T15753c.hs:55:9: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    16 
    +    Pattern match(es) are non-exhaustive
    17 
    +    In a case alternative:
    18 
    +        Patterns of type ‘SUnit u2’ not matched: SUnit
    19 
    +

  • testsuite/tests/pmcheck/should_compile/T15753d.hs
    ... ... @@ -8,7 +8,11 @@
    8 8 
     {-# LANGUAGE TypeOperators #-}
    9 9 
     {-# LANGUAGE UndecidableInstances #-}
    10 10 
     {-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
    11 
    -module Bug where
    11 
    +
    12 
    +-- NB: After fixing #22652 this program right produces warnings
    13 
    +-- But it produces too many warnings: #26685
    14 
    +
    15 
    +module T15753d where
    12 16
    13 17 
     import Data.Kind
    14 18 
     import Data.Type.Bool

  • testsuite/tests/pmcheck/should_compile/T15753d.stderr
    1 
    +T15753d.hs:83:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
    2 
    +    Pattern match has inaccessible right hand side
    3 
    +    In an equation for ‘mapInsertWithNonEmpty1’:
    4 
    +        mapInsertWithNonEmpty1 sf
    5 
    +                               snew_k
    6 
    +                               snew_v
    7 
    +                               (SMkMap sm)
    8 
    +                               Refl
    9 
    +                               Refl | STuple2 sold_k _ `SCons` sold_kvs <- sm,
    10 
    +                                      SFalse <- sold_k %== snew_k = ...
    11 
    +
    12 
    +T15753d.hs:85:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    13 
    +    Pattern match(es) are non-exhaustive
    14 
    +    In a case alternative:
    15 
    +        Patterns of type ‘Sing
    16 
    +                            (MapInsertWith f new_k new_v (MkMap xs))’ not matched:
    17 
    +            SMkMap _
    18 
    +
    19 
    +T15753d.hs:95:5: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
    20 
    +    Pattern match has inaccessible right hand side
    21 
    +    In an equation for ‘mapInsertWithNonEmpty2’:
    22 
    +        mapInsertWithNonEmpty2 sf
    23 
    +                               snew_k
    24 
    +                               snew_v
    25 
    +                               (SMkMap sm)
    26 
    +                               Refl
    27 
    +                               Refl | STuple2 sold_k _ `SCons` sold_kvs <- sm = ...
    28 
    +
    29 
    +T15753d.hs:96:5: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    30 
    +    Pattern match(es) are non-exhaustive
    31 
    +    In a case alternative:
    32 
    +        Patterns of type ‘Sing (x == new_k)’ not matched: STrue
    33 
    +
    34 
    +T15753d.hs:98:9: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    35 
    +    Pattern match(es) are non-exhaustive
    36 
    +    In a case alternative:
    37 
    +        Patterns of type ‘Sing
    38 
    +                            (MapInsertWith f new_k new_v (MkMap xs))’ not matched:
    39 
    +            SMkMap _
    40 
    +

  • testsuite/tests/pmcheck/should_compile/T22652a.hs
    1 
    +{-# LANGUAGE DataKinds #-}
    2 
    +{-# LANGUAGE EmptyCase #-}
    3 
    +{-# LANGUAGE GADTs #-}
    4 
    +{-# LANGUAGE TypeFamilies #-}
    5 
    +{-# LANGUAGE TypeOperators #-}
    6 
    +{-# LANGUAGE UndecidableInstances #-}
    7 
    +{-# OPTIONS_GHC -Wincomplete-patterns #-}
    8 
    +
    9 
    +-- This test is a spin-off from the test T15753c
    10 
    +
    11 
    +module T22652a where
    12 
    +
    13 
    +import Data.Kind (Type)
    14 
    +import Data.Type.Equality ((:~:)(..))
    15 
    +import Data.Void (Void)
    16 
    +
    17 
    +data SBool :: Bool -> Type where
    18 
    +  SFalse :: SBool False
    19 
    +  STrue  :: SBool True
    20 
    +
    21 
    +data SUnit :: () -> Type where
    22 
    +  SUnit :: SUnit '()
    23 
    +
    24 
    +type family IsUnit (u :: ()) :: Bool where
    25 
    +  IsUnit '() = True
    26 
    +
    27 
    +type family If (c :: Bool) (t :: Type) (f :: Type) :: Type where
    28 
    +  If True  t _ = t
    29 
    +  If False _ f = f
    30 
    +
    31 
    +type family F (u1 :: ()) (u2 :: ()) :: Type where
    32 
    +  F u1 u2 =
    33 
    +    If (IsUnit u1) (Case u2) Int
    34 
    +
    35 
    +type family Case (u :: ()) :: Type where
    36 
    +  Case '() = Int
    37 
    +
    38 
    +---------------------------------------
    39 
    +-- The checker can (now, Dec 25) see that (F u1 u2 ~ Char) is
    40 
    +-- unsatisfiable, so the empty pattern match is fine
    41 
    +g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void
    42 
    +g1a r _ _ = case r of {}
    43 
    +
    44 
    +{- Why   [G] F u1 u2 ~ Char  is unsatisfiable
    45 
    +
    46 
    +[G] F u1 u2 ~ Char =>rewrite   [G] If (IsUnit u1) (Case u2) Int ~ Char
    47 
    +                   =>(fundep)  [W] IsUnit u1 ~ True
    48 
    +                               [W] Case u2 ~ Char   <<--  insoluble: no relevant eqns
    49 
    +-}

  • testsuite/tests/pmcheck/should_compile/all.T
    ... ... @@ -180,3 +180,4 @@ test('T24891', normal, compile, ['-Wincomplete-record-selectors'])
    180 180 
     test('T25257', normal, compile, [overlapping_incomplete])
    181 181 
     test('T24845', [], compile, [overlapping_incomplete])
    182 182 
     test('T22652', [], compile, [overlapping_incomplete])
    183 
    +test('T22652a', [], compile, [overlapping_incomplete])

  • testsuite/tests/typecheck/should_fail/T5236.stderr
    1 
    +T5236.hs:16:9: error: [GHC-39999]
    2 
    +    • No instance for ‘Id A B’
    3 
    +      The functional dependencies arising from this constraint are insoluble
    4 
    +    • In the ambiguity check for ‘loop’
    5 
    +      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    6 
    +      In the type signature: loop :: Id A B => Bool
    7 
    +

  • testsuite/tests/typecheck/should_fail/all.T
    ... ... @@ -250,7 +250,7 @@ test('SilentParametersOverlapping', normal, compile, [''])
    250 250 
     test('FailDueToGivenOverlapping', normal, compile_fail, [''])
    251 251 
     test('LongWayOverlapping', normal, compile_fail, [''])
    252 252 
     test('T5051', normal, compile, [''])
    253 
    -test('T5236',normal,compile,[''])
    253 
    +test('T5236',normal,compile_fail,[''])
    254 254 
     test('T5246',normal,compile_fail,[''])
    255 255 
     test('T5300',normal,compile_fail,[''])
    256 256 
     test('T5095',normalise_fun(normalise_errmsg),compile_fail,[''])

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