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

Commits:

8 changed files:

Changes:

  • compiler/GHC/Tc/Solver/Default.hs
    ... ... @@ -485,13 +485,14 @@ defaultEquality encl_eqs ct
    485 485
    486 486 
                ReprEq -- See Note [Defaulting representational equalities]
    487 487
    488 
    -                  -- Don't even try this for definitely-insoluble representational
    489 
    -                  -- equalities such as Int ~R# Bool.
    488 
    +                  -- Don't even try this for definitely-insoluble
    489 
    +                  -- representational equalities such as Int ~R# Bool.
    490 490 
                       | CIrredCan (IrredCt { ir_reason }) <- ct
    491 491 
                       , isInsolubleReason ir_reason
    492 492 
                       -> return False
    493 493
    494 494 
                       -- Nor if there are enclosing equalities
    495 
    +                  -- See (DRE1) in Note [Defaulting representational equalities]
    495 496 
                       | encl_eqs
    496 497 
                       -> return False
    497 498
    ... ... @@ -697,15 +698,7 @@ Wrinkles:
    697 698
    698 699 
       See #10009, and Note [Limited defaulting in the ambiguity check].
    699 700
    700 
    -
    701 
    -Note [Must simplify after defaulting]
    702 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    703 
    -We may have a deeply buried constraint
    704 
    -    (t:*) ~ (a:Open)
    705 
    -which we couldn't solve because of the kind incompatibility, and 'a' is free.
    706 
    -Then when we default 'a' we can solve the constraint.  And we want to do
    707 
    -that before starting in on type classes.  We MUST do it before reporting
    708 
    -errors, because it isn't an error!  #7967 was due to this.
    701 
    +(DE7) For representational equalities see Note [Defaulting representational equalities]
    709 702
    710 703 
     Note [Defaulting representational equalities]
    711 704 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -766,6 +759,23 @@ in which case unifying alpha := Int would be wrong, as the correct solution is
    766 759 
     alpha := Age. This worry doesn't concern us in top-level defaulting, because
    767 760 
     defaulting takes place after generalisation; it is fully monomorphic.
    768 761
    762 
    +(DRE1) Suppose we have (see test UnliftedNewtypesCoerceFail)
    763 
    +         [G] Coercible a b
    764 
    +         [W] alpha ~R# beta
    765 
    +  Then we don't want to make alpha:=beta, because we probably should really solve it
    766 
    +  from the Given Coercible constraint.  So we check first for the absence of enclosing
    767 
    +  equalities.  This is a bit ad-hoc, but so is all of defaulting really.
    768 
    +
    769 
    +Note [Must simplify after defaulting]
    770 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    771 
    +We may have a deeply buried constraint
    772 
    +    (t:*) ~ (a:Open)
    773 
    +which we couldn't solve because of the kind incompatibility, and 'a' is free.
    774 
    +Then when we default 'a' we can solve the constraint.  And we want to do
    775 
    +that before starting in on type classes.  We MUST do it before reporting
    776 
    +errors, because it isn't an error!  #7967 was due to this.
    777 
    +
    778 
    +
    769 779 
     *********************************************************************************
    770 780 
     *                                                                               *
    771 781 
     *                Type-class defaulting

  • compiler/GHC/Tc/Solver/InertSet.hs
    ... ... @@ -24,7 +24,7 @@ module GHC.Tc.Solver.InertSet (
    24 24 
         -- * Inert equalities
    25 25 
         InertEqs,
    26 26 
         foldTyEqs, delEq, findEq,
    27 
    -    partitionInertEqs, partitionFunEqs,
    27 
    +    partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs,
    28 28 
         filterInertEqs, filterFunEqs,
    29 29 
         foldFunEqs, addEqToCans,
    30 30
    ... ... @@ -1359,27 +1359,30 @@ findEq icans (TyVarLHS tv) = findTyEqs icans tv
    1359 1359 
     findEq icans (TyFamLHS fun_tc fun_args)
    1360 1360 
       = concat @Maybe (findFunEq (inert_funeqs icans) fun_tc fun_args)
    1361 1361
    1362 
    -{-# INLINE partition_eqs_container #-}
    1363 
    -partition_eqs_container
    1364 
    -  :: forall container
    1365 
    -   . container    -- empty container
    1366 
    -  -> (forall b. (EqCt -> b -> b) ->  container -> b -> b) -- folder
    1367 
    -  -> (EqCt -> container -> container)  -- extender
    1368 
    -  -> (EqCt -> Bool)
    1369 
    -  -> container
    1370 
    -  -> ([EqCt], container)
    1371 
    -partition_eqs_container empty_container fold_container extend_container pred orig_inerts
    1372 
    -  = fold_container folder orig_inerts ([], empty_container)
    1362 
    +transformAndPartitionTyVarEqs
    1363 
    +  :: (EqCt -> Either EqCt EqCt)         -- Left => chuck out, Right => keep
    1364 
    +  -> InertEqs
    1365 
    +  -> ([EqCt], InertEqs)               -- (chuck-out, keep)
    1366 
    +transformAndPartitionTyVarEqs pred orig_inerts
    1367 
    +  = foldTyEqs folder orig_inerts ([], emptyTyEqs)
    1373 1368 
       where
    1374 
    -    folder :: EqCt -> ([EqCt], container) -> ([EqCt], container)
    1369 
    +    folder :: EqCt -> ([EqCt], InertEqs) -> ([EqCt], InertEqs)
    1375 1370 
         folder eq_ct (acc_true, acc_false)
    1376 
    -      | pred eq_ct = (eq_ct : acc_true, acc_false)
    1377 
    -      | otherwise  = (acc_true,         extend_container eq_ct acc_false)
    1371 
    +      = case pred eq_ct of
    1372 
    +           Left eq_ct'  -> (eq_ct' : acc_true, acc_false)
    1373 
    +           Right eq_ct' -> (acc_true, addInertEqs eq_ct' acc_false)
    1378 1374
    1379 1375 
     partitionInertEqs :: (EqCt -> Bool)   -- EqCt will always have a TyVarLHS
    1380 1376 
                       -> InertEqs
    1381 1377 
                       -> ([EqCt], InertEqs)
    1382 
    -partitionInertEqs = partition_eqs_container emptyTyEqs foldTyEqs addInertEqs
    1378 
    +partitionInertEqs pred orig_inerts
    1379 
    +  = foldTyEqs folder orig_inerts ([], emptyTyEqs)
    1380 
    +  where
    1381 
    +    folder :: EqCt -> ([EqCt], InertEqs) -> ([EqCt], InertEqs)
    1382 
    +    folder eq_ct (acc_true, acc_false)
    1383 
    +      = case pred eq_ct of
    1384 
    +           True  -> (eq_ct : acc_true, acc_false)
    1385 
    +           False -> (acc_true, addInertEqs eq_ct acc_false)
    1383 1386
    1384 1387 
     addInertEqs :: EqCt -> InertEqs -> InertEqs
    1385 1388 
     -- Precondition: CanEqLHS is a TyVarLHS
    ... ... @@ -1412,7 +1415,14 @@ foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z
    1412 1415 
     partitionFunEqs :: (EqCt -> Bool)    -- EqCt will have a TyFamLHS
    1413 1416 
                     -> InertFunEqs
    1414 1417 
                     -> ([EqCt], InertFunEqs)
    1415 
    -partitionFunEqs = partition_eqs_container emptyFunEqs foldFunEqs addFunEqs
    1418 
    +partitionFunEqs pred orig_inerts
    1419 
    +  = foldFunEqs folder orig_inerts ([], emptyFunEqs)
    1420 
    +  where
    1421 
    +    folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs)
    1422 
    +    folder eq_ct (acc_true, acc_false)
    1423 
    +      = case pred eq_ct of
    1424 
    +           True  -> (eq_ct : acc_true, acc_false)
    1425 
    +           False -> (acc_true, addFunEqs eq_ct acc_false)
    1416 1426
    1417 1427 
     addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs
    1418 1428 
     -- Precondition: EqCt is a TyFamLHS
    ... ... @@ -1424,12 +1434,11 @@ addFunEqs other _ = pprPanic "extendFunEqs" (ppr other)
    1424 1434 
     filterFunEqs :: (EqCt -> Bool) -> InertFunEqs -> InertFunEqs
    1425 1435 
     filterFunEqs f = mapMaybeTcAppMap g
    1426 1436 
       where
    1427 
    -    g xs =
    1428 
    -      let filtered = filter f xs
    1429 
    -      in
    1430 
    -        if null filtered
    1431 
    -        then Nothing
    1432 
    -        else Just filtered
    1437 
    +    g xs | null filtered = Nothing
    1438 
    +         | otherwise     = Just filtered
    1439 
    +         where
    1440 
    +           filtered = filter f xs
    1441 
    +
    1433 1442
    1434 1443 
     {- *********************************************************************
    1435 1444 
     *                                                                      *

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -190,7 +190,6 @@ import GHC.Types.DefaultEnv ( DefaultEnv )
    190 190 
     import GHC.Types.Var
    191 191 
     import GHC.Types.Var.Set
    192 192 
     import GHC.Types.Unique.Supply
    193 
    -import GHC.Types.Unique.Set( elementOfUniqSet )
    194 193 
     import GHC.Types.Id
    195 194 
     import GHC.Types.Basic (allImportLevels)
    196 195 
     import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel)
    ... ... @@ -458,15 +457,16 @@ kickOutAfterUnification tv_set
    458 457 
            ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked)
    459 458 
            ; return n_kicked }
    460 459
    461 
    -kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
    460 
    +kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
    462 461 
     -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty]
    463 462 
     -- in GHC.Tc.Solver.Equality
    464 463 
     --
    465 464 
     -- It's possible that this could just go ahead and unify, but could there
    466 465 
     -- be occurs-check problems? Seems simpler just to kick out.
    467 
    -kickOutAfterFillingCoercionHole hole
    466 
    +kickOutAfterFillingCoercionHole hole co
    468 467 
       = do { ics <- getInertCans
    469 
    -       ; let (kicked_out, ics') = kick_out ics
    468 
    +       ; new_holes <- liftZonkTcS $ TcM.freeHolesOfCoercion co
    469 
    +       ; let (kicked_out, ics') = kick_out new_holes ics
    470 470 
                  n_kicked           = length kicked_out
    471 471
    472 472 
            ; unless (n_kicked == 0) $
    ... ... @@ -479,20 +479,25 @@ kickOutAfterFillingCoercionHole hole
    479 479
    480 480 
            ; setInertCans ics' }
    481 481 
       where
    482 
    -    kick_out :: InertCans -> ([EqCt], InertCans)
    483 
    -    kick_out ics@(IC { inert_eqs = eqs })
    482 
    +    kick_out :: RewriterSet -> InertCans -> ([EqCt], InertCans)
    483 
    +    kick_out new_holes ics@(IC { inert_eqs = eqs })
    484 484 
           = (eqs_to_kick, ics { inert_eqs = eqs_to_keep })
    485 485 
           where
    486 
    -        (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_out_eq eqs
    486 
    +        (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs (kick_out_eq new_holes) eqs
    487 487
    488 
    -    kick_out_eq :: EqCt -> Bool    -- True: kick out; False: keep.
    489 
    -    kick_out_eq (EqCt { eq_ev = ev ,eq_lhs = lhs })
    490 
    -      | CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev
    488 
    +    kick_out_eq :: RewriterSet -> EqCt -> Either EqCt EqCt
    489 
    +    kick_out_eq new_holes eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs })
    490 
    +      | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev
    491 491 
           , TyVarLHS tv <- lhs
    492 492 
           , isMetaTyVar tv
    493 
    -      = hole `elementOfUniqSet` rewriters
    493 
    +      , hole `elemRewriterSet` rewriters
    494 
    +      , let holes' = (rewriters `delRewriterSet` hole) `mappend` new_holes
    495 
    +            eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }
    496 
    +      = if isEmptyRewriterSet holes'
    497 
    +        then Left eq_ct'    -- Kick out
    498 
    +        else Right eq_ct'   -- Keep, but with trimmed holes
    494 499 
           | otherwise
    495 
    -      = False
    500 
    +      = Right eq_ct
    496 501
    497 502 
     --------------
    498 503 
     insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
    ... ... @@ -1990,7 +1995,7 @@ Yuk!
    1990 1995 
     fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
    1991 1996 
     fillCoercionHole hole co
    1992 1997 
       = do { wrapTcS $ TcM.fillCoercionHole hole co
    1993 
    -       ; kickOutAfterFillingCoercionHole hole }
    1998 
    +       ; kickOutAfterFillingCoercionHole hole co }
    1994 1999
    1995 2000 
     setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
    1996 2001 
     setEvBindIfWanted ev canonical tm

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -88,9 +88,10 @@ module GHC.Tc.Types.Constraint (
    88 88 
             GivenCtEvidence(..), WantedCtEvidence(..),
    89 89
    90 90 
             -- RewriterSet
    91 
    -        RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet,
    92 
    -           -- exported concretely only for zonkRewriterSet
    91 
    +        --   RewriterSet(..) is exported concretely only for zonkRewriterSet
    92 
    +        RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet,
    93 93 
             addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts,
    94 
    +        delRewriterSet,
    94 95
    95 96 
             wrapType,
    96 97
    ... ... @@ -2506,6 +2507,12 @@ emptyRewriterSet = RewriterSet emptyUniqSet
    2506 2507 
     unitRewriterSet :: CoercionHole -> RewriterSet
    2507 2508 
     unitRewriterSet = coerce (unitUniqSet @CoercionHole)
    2508 2509
    2510 
    +elemRewriterSet :: CoercionHole -> RewriterSet -> Bool
    2511 
    +elemRewriterSet = coerce (elementOfUniqSet @CoercionHole)
    2512 
    +
    2513 
    +delRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet
    2514 
    +delRewriterSet = coerce (delOneFromUniqSet @CoercionHole)
    2515 
    +
    2509 2516 
     unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet
    2510 2517 
     unionRewriterSet = coerce (unionUniqSets @CoercionHole)
    2511 2518

  • compiler/GHC/Tc/Zonk/TcType.hs
    ... ... @@ -43,6 +43,7 @@ module GHC.Tc.Zonk.TcType
    43 43
    44 44 
         -- * Coercion holes
    45 45 
       , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe
    46 
    +  , freeHolesOfCoercion
    46 47
    47 48
    48 49 
         -- * Tidying
    ... ... @@ -583,30 +584,33 @@ zonkCtEvRewriterSet ev@(CtWanted wtd)
    583 584 
     -- find all the free un-filled coercion holes in the coercion that fills it
    584 585 
     zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet
    585 586 
     zonkRewriterSet (RewriterSet set)
    586 
    -  = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set
    587 
    +  = unUCHM (nonDetStrictFoldUniqSet go mempty set)
    587 588 
          -- This does not introduce non-determinism, because the only
    588 589 
          -- monadic action is to read, and the combining function is
    589 590 
          -- commutative
    590 591 
       where
    591 
    -    go :: CoercionHole -> ZonkM RewriterSet -> ZonkM RewriterSet
    592 
    -    go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc
    593 
    -
    594 
    -    check_hole :: CoercionHole -> ZonkM RewriterSet
    595 
    -    check_hole hole
    596 
    -      = do { m_co <- unpackCoercionHole_maybe hole
    597 
    -           ; case m_co of
    598 
    -               Nothing -> return (unitRewriterSet hole)  -- Not filled
    599 
    -               Just co -> unUCHM (check_co co) }         -- Filled: look inside
    600 
    -
    601 
    -    check_ty :: Type -> UnfilledCoercionHoleMonoid
    602 
    -    check_co :: Coercion -> UnfilledCoercionHoleMonoid
    603 
    -    (check_ty, _, check_co, _) = foldTyCo folder ()
    604 
    -
    605 
    -    folder :: TyCoFolder () UnfilledCoercionHoleMonoid
    606 
    -    folder = TyCoFolder { tcf_view  = noView
    607 
    -                        , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv)
    608 
    -                        , tcf_covar = \ _ cv -> check_ty (varType cv)
    609 
    -                        , tcf_hole  = \ _ -> UCHM . check_hole
    592 
    +    go :: CoercionHole -> UnfilledCoercionHoleMonoid -> UnfilledCoercionHoleMonoid
    593 
    +    go hole m_acc = freeHolesOfHole hole `mappend` m_acc
    594 
    +
    595 
    +freeHolesOfCoercion :: Coercion -> ZonkM RewriterSet
    596 
    +freeHolesOfCoercion co = unUCHM (freeHolesOfCo co)
    597 
    +
    598 
    +freeHolesOfHole :: CoercionHole -> UnfilledCoercionHoleMonoid
    599 
    +freeHolesOfHole hole
    600 
    +  = UCHM $ do { m_co <- unpackCoercionHole_maybe hole
    601 
    +              ; case m_co of
    602 
    +                   Nothing -> return (unitRewriterSet hole)  -- Not filled
    603 
    +                   Just co -> unUCHM (freeHolesOfCo co) }    -- Filled: look inside
    604 
    +
    605 
    +freeHolesOfTy :: Type     -> UnfilledCoercionHoleMonoid
    606 
    +freeHolesOfCo :: Coercion -> UnfilledCoercionHoleMonoid
    607 
    +(freeHolesOfTy, _, freeHolesOfCo, _) = foldTyCo freeHolesFolder ()
    608 
    +
    609 
    +freeHolesFolder :: TyCoFolder () UnfilledCoercionHoleMonoid
    610 
    +freeHolesFolder = TyCoFolder { tcf_view  = noView
    611 
    +                        , tcf_tyvar = \ _ tv -> freeHolesOfTy (tyVarKind tv)
    612 
    +                        , tcf_covar = \ _ cv -> freeHolesOfTy (varType cv)
    613 
    +                        , tcf_hole  = \ _ h  -> freeHolesOfHole h
    610 614 
                             , tcf_tycobinder = \ _ _ _ -> () }
    611 615
    612 616 
     newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet }

  • testsuite/tests/rep-poly/RepPolyNPlusK.stderr
    ... ... @@ -9,21 +9,21 @@ RepPolyNPlusK.hs:22:6: error: [GHC-55287]
    9 9 
               arising from the literal ‘2’
    10 10 
             does not have a fixed runtime representation.
    11 11 
             Its type is:
    12 
    -          a0 :: TYPE rep0
    12 
    +          a1 :: TYPE rep2
    13 13 
             When unifying:
    14 
    -          • a0
    14 
    +          • a1
    15 15 
               • a
    16 
    -        Cannot unify ‘rep1’ with the type variable ‘rep0’
    16 
    +        Cannot unify ‘rep1’ with the type variable ‘rep2’
    17 17 
             because the former is not a concrete ‘RuntimeRep’.
    18 18 
           • The first argument of the rebindable syntax operator ‘(-)’
    19 19 
               arising from the literal ‘2’
    20 20 
             does not have a fixed runtime representation.
    21 21 
             Its type is:
    22 
    -          a1 :: TYPE rep2
    22 
    +          a0 :: TYPE rep0
    23 23 
             When unifying:
    24 
    -          • a1
    24 
    +          • a0
    25 25 
               • a
    26 
    -        Cannot unify ‘rep1’ with the type variable ‘rep2’
    26 
    +        Cannot unify ‘rep1’ with the type variable ‘rep0’
    27 27 
             because the former is not a concrete ‘RuntimeRep’.
    28 28 
         • In the pattern: bndr_a+2
    29 29 
           In an equation for ‘foo’: foo (bndr_a+2) = ()

  • testsuite/tests/rep-poly/T14561b.stderr
    ... ... @@ -2,9 +2,9 @@ T14561b.hs:12:9: error: [GHC-55287]
    2 2 
         • The first argument of ‘coerce’
    3 3 
           does not have a fixed runtime representation.
    4 4 
           Its type is:
    5 
    -        a0 :: TYPE k0
    5 
    +        b0 :: TYPE k0
    6 6 
           When unifying:
    7 
    -        • a0 -> b0
    7 
    +        • b0 -> b0
    8 8 
             • a -> a
    9 9 
           Cannot unify ‘r’ with the type variable ‘k0’
    10 10 
           because the former is not a concrete ‘RuntimeRep’.

  • testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
    ... ... @@ -2,9 +2,9 @@ UnliftedNewtypesCoerceFail.hs:14:8: error: [GHC-55287]
    2 2 
         • The first argument of ‘coerce’
    3 3 
           does not have a fixed runtime representation.
    4 4 
           Its type is:
    5 
    -        b0 :: TYPE k0
    5 
    +        a0 :: TYPE k0
    6 6 
           When unifying:
    7 
    -        • b0 -> b0
    7 
    +        • a0 -> b0
    8 8 
             • x -> y
    9 9 
           Cannot unify ‘rep’ with the type variable ‘k0’
    10 10 
           because the former is not a concrete ‘RuntimeRep’.

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