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

Commits:

15 changed files:

Changes:

  • compiler/GHC/Core/FamInstEnv.hs
    ... ... @@ -1061,10 +1061,10 @@ lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys
    1061 1061 
                                 , fi_tys = tpl_tys }) =  do
    1062 1062 
           subst <- tcMatchTys tpl_tys match_tys1
    1063 1063 
           return (FamInstMatch { fim_instance = item
    1064 
    -                             , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
    1065 
    -                             , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
    1066 
    -                                               substCoVars subst tpl_cvs
    1067 
    -                             })
    1064 
    +                           , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2
    1065 
    +                           , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
    1066 
    +                                            substCoVars subst tpl_cvs
    1067 
    +                           })
    1068 1068 
             where
    1069 1069 
               (match_tys1, match_tys2) = split_tys tpl_tys
    1070 1070

  • compiler/GHC/Tc/Instance/Family.hs
    ... ... @@ -5,7 +5,7 @@ module GHC.Tc.Instance.Family (
    5 5 
             FamInstEnvs, tcGetFamInstEnvs,
    6 6 
             checkFamInstConsistency, tcExtendLocalFamInstEnv,
    7 7 
             tcLookupDataFamInst, tcLookupDataFamInst_maybe,
    8 
    -        tcTopNormaliseNewTypeTF_maybe,
    8 
    +        tcUnwrapNewtype_maybe,
    9 9
    10 10 
             -- * Injectivity
    11 11 
             reportInjectivityErrors, reportConflictingInjectivityErrs
    ... ... @@ -46,7 +46,6 @@ import GHC.Utils.Misc
    46 46 
     import GHC.Utils.Panic
    47 47 
     import GHC.Utils.FV
    48 48
    49 
    -import GHC.Data.Bag( Bag, unionBags, unitBag )
    50 49 
     import GHC.Data.Maybe
    51 50
    52 51 
     import Control.Monad
    ... ... @@ -452,58 +451,57 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
    452 451 
       | otherwise
    453 452 
       = Nothing
    454 453
    455 
    --- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
    456 
    --- potentially looking through newtype /instances/ and type synonyms.
    454 
    +-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes
    457 455 
     --
    458 456 
     -- It is only used by the type inference engine (specifically, when
    459 457 
     -- solving representational equality), and hence it is careful to unwrap
    460 458 
     -- only if the relevant data constructor is in scope.  That's why
    461 459 
     -- it gets a GlobalRdrEnv argument.
    462 460 
     --
    463 
    --- It is careful not to unwrap data/newtype instances nor synonyms
    464 
    --- if it can't continue unwrapping.  Such care is necessary for proper
    465 
    --- error messages.
    461 
    +-- It is capable of unwrapping a newtype /instance/.  E.g
    462 
    +--    data D a
    463 
    +--    newtype instance D Int = MkD Bool
    464 
    +-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside.
    465 
    +-- However, it is careful not to unwrap data/newtype instances if it can't
    466 
    +-- unwrap the newtype inside it; that might in the example if `MkD` was
    467 
    +-- not in scope.  Such care is necessary for proper error messages.
    466 468 
     --
    467 469 
     -- It does not look through type families.
    468 
    --- It does not normalise arguments to a tycon.
    470 
    +-- It does not normalise arguments to the tycon.
    469 471 
     --
    470 
    --- If the result is Just ((gres, co), rep_ty), then
    472 
    +-- If the result is Just (gre, co, rep_ty), then
    471 473 
     --    co : ty ~R rep_ty
    472 
    ---    gres are the GREs for the data constructors that
    473 
    ---                          had to be in scope
    474 
    -tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
    475 
    -                              -> GlobalRdrEnv
    476 
    -                              -> Type
    477 
    -                              -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
    478 
    -tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
    479 
    --- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
    480 
    -  = topNormaliseTypeX stepper plus ty
    474 
    +--    gre is the GRE for the data constructor that had to be in scope
    475 
    +tcUnwrapNewtype_maybe :: FamInstEnvs
    476 
    +                      -> GlobalRdrEnv
    477 
    +                      -> Type
    478 
    +                      -> Maybe (GlobalRdrElt, TcCoercion, Type)
    479 
    +tcUnwrapNewtype_maybe faminsts rdr_env ty
    480 
    +  | Just (tc,tys) <- tcSplitTyConApp_maybe ty
    481 
    +  = firstJust (try_nt_unwrap tc tys)
    482 
    +              (try_fam_unwrap tc tys)
    483 
    +  | otherwise
    484 
    +  = Nothing
    481 485 
       where
    482 
    -    plus :: (Bag GlobalRdrElt, TcCoercion) -> (Bag GlobalRdrElt, TcCoercion)
    483 
    -         -> (Bag GlobalRdrElt, TcCoercion)
    484 
    -    plus (gres1, co1) (gres2, co2) = ( gres1 `unionBags` gres2
    485 
    -                                     , co1 `mkTransCo` co2 )
    486 
    -
    487 
    -    stepper :: NormaliseStepper (Bag GlobalRdrElt, TcCoercion)
    488 
    -    stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
    489 
    -
    490 
    -    -- For newtype instances we take a double step or nothing, so that
    486 
    +    -- For newtype /instances/ we take a double step or nothing, so that
    491 487 
         -- we don't return the representation type of the newtype instance,
    492 488 
         -- which would lead to terrible error messages
    493 
    -    unwrap_newtype_instance rec_nts tc tys
    494 
    -      | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
    495 
    -      = fmap (mkTransCo co) <$> unwrap_newtype rec_nts tc' tys'
    496 
    -      | otherwise = NS_Done
    489 
    +    try_fam_unwrap tc tys
    490 
    +      | Just (tc', tys', fam_co) <- tcLookupDataFamInst_maybe faminsts tc tys
    491 
    +      , Just (gre, nt_co, ty') <- try_nt_unwrap tc' tys'
    492 
    +      = Just (gre, mkTransCo fam_co nt_co, ty')
    493 
    +      | otherwise
    494 
    +      = Nothing
    497 495
    498 
    -    unwrap_newtype rec_nts tc tys
    496 
    +    try_nt_unwrap tc tys
    499 497 
           | Just con <- newTyConDataCon_maybe tc
    500 498 
           , Just gre <- lookupGRE_Name rdr_env (dataConName con)
    501 499 
                -- This is where we check that the
    502 500 
                -- data constructor is in scope
    503 
    -      = (,) (unitBag gre) <$> unwrapNewTypeStepper rec_nts tc tys
    504 
    -
    501 
    +      , Just (ty', co) <- instNewTyCon_maybe tc tys
    502 
    +      = Just (gre, co, ty')
    505 503 
           | otherwise
    506 
    -      = NS_Done
    504 
    +      = Nothing
    507 505
    508 506 
     {-
    509 507 
     ************************************************************************

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -23,7 +23,7 @@ import GHC.Tc.Types.CtLoc
    23 23 
     import GHC.Tc.Types.Origin
    24 24 
     import GHC.Tc.Utils.Unify
    25 25 
     import GHC.Tc.Utils.TcType
    26 
    -import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
    26 
    +import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe )
    27 27 
     import qualified GHC.Tc.Utils.Monad    as TcM
    28 28
    29 29 
     import GHC.Core.Type
    ... ... @@ -48,7 +48,6 @@ import GHC.Utils.Misc
    48 48 
     import GHC.Utils.Monad
    49 49
    50 50 
     import GHC.Data.Pair
    51 
    -import GHC.Data.Bag
    52 51 
     import Control.Monad
    53 52 
     import Data.Maybe ( isJust, isNothing )
    54 53 
     import Data.List  ( zip4 )
    ... ... @@ -334,24 +333,52 @@ can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
    334 333 
       | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2  ps_ty2
    335 334 
       | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1  ps_ty1 ty2' ps_ty2
    336 335
    337 
    --- need to check for reflexivity in the ReprEq case.
    338 
    --- See Note [Eager reflexivity check]
    339 
    --- Check only when rewritten because the zonk_eq_types check in canEqNC takes
    340 
    --- care of the non-rewritten case.
    341 
    -can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _
    342 
    -  | ty1 `tcEqType` ty2
    343 
    -  = canEqReflexive ev ReprEq ty1
    344 
    -
    345 
    --- When working with ReprEq, unwrap newtypes.
    346 
    --- See Note [Unwrap newtypes first]
    336 
    +-- Look for (N s1 .. sn) ~R# (N t1 .. tn)
    337 
    +-- where either si=ti
    338 
    +--       or     N is phantom in i'th position
    339 
    +-- See Note [Solving newtype equalities: overview]
    340 
    +-- and (for details) Note [Eager newtype decomposition]
    341 
    +-- We try this /before/ attempting to unwrap N, because if N is
    342 
    +-- recursive, unwrapping will loop.
    343 
    +-- This /matters/ for newtypes, but is /safe/ for all types
    344 
    +can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
    345 
    +  | ReprEq <- eq_rel
    346 
    +  , TyConApp tc1 tys1 <- ty1
    347 
    +  , TyConApp tc2 tys2 <- ty2
    348 
    +  , tc1 == tc2
    349 
    +  , ok tys1 tys2 (tyConRoles tc1)
    350 
    +  = canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2)
    351 
    +  where
    352 
    +    ok :: [TcType] -> [TcType] -> [Role] -> Bool
    353 
    +    -- OK to decompose a representational equality
    354 
    +    --   if the args are already equal
    355 
    +    --   or are phantom role
    356 
    +    -- See Note [Eager newtype decomposition]
    357 
    +    -- You might think that representational role would also be OK, but
    358 
    +    --   see Note [Even more eager newtype decomposition]
    359 
    +    ok (ty1:tys1) (ty2:tys2) rs
    360 
    +      | Phantom : rs' <- rs = ok tys1 tys2 rs'
    361 
    +      | ty1 `tcEqType` ty2  = ok tys1 tys2 (drop 1 rs)
    362 
    +      | otherwise           = False
    363 
    +    ok [] [] _  = True
    364 
    +    ok _  _  _  = False  -- Mis-matched lengths, just about possible because of
    365 
    +                         -- kind polymorphism.  Anyway False is a safe result!
    366 
    +
    367 
    +-- Unwrap newtypes, when in ReprEq only
    368 
    +-- See Note [Solving newtype equalities: overview]
    369 
    +-- and (for details) Note [Unwrap newtypes first]
    347 370 
     -- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
    371 
    +--
    372 
    +-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to
    373 
    +-- `can_eq_nc`.  If there is a recursive newtype, so that we keep
    374 
    +-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up.
    348 375 
     can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
    349 376 
       | ReprEq <- eq_rel
    350 
    -  , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
    377 
    +  , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1
    351 378 
       = can_eq_newtype_nc rdr_env envs ev NotSwapped stuff1 ty2 ps_ty2
    352 379
    353 380 
       | ReprEq <- eq_rel
    354 
    -  , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
    381 
    +  , Just stuff2 <- tcUnwrapNewtype_maybe envs rdr_env ty2
    355 382 
       = can_eq_newtype_nc rdr_env envs ev IsSwapped stuff2 ty1 ps_ty1
    356 383
    357 384 
     -- Then, get rid of casts
    ... ... @@ -374,6 +401,11 @@ can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
    374 401 
       = do { setEqIfWanted ev (mkReflCPH eq_rel ty1)
    375 402 
            ; stopWith ev "Equal LitTy" }
    376 403
    404 
    +can_eq_nc _rewritten _rdr_env _envs ev eq_rel
    405 
    +           s1@ForAllTy{} _
    406 
    +           s2@ForAllTy{} _
    407 
    +  = can_eq_nc_forall ev eq_rel s1 s2
    408 
    +
    377 409 
     -- Decompose FunTy: (s -> t) and (c => t)
    378 410 
     -- NB: don't decompose (Int -> blah) ~ (Show a => blah)
    379 411 
     can_eq_nc _rewritten _rdr_env _envs ev eq_rel
    ... ... @@ -401,19 +433,20 @@ can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
    401 433 
       , rewritten || both_generative
    402 434 
       = canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2)
    403 435
    404 
    -can_eq_nc _rewritten _rdr_env _envs ev eq_rel
    405 
    -           s1@ForAllTy{} _
    406 
    -           s2@ForAllTy{} _
    407 
    -  = can_eq_nc_forall ev eq_rel s1 s2
    408 
    -
    409 
    --- See Note [Canonicalising type applications] about why we require rewritten types
    410 
    --- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
    411 
    --- NB: Only decompose AppTy for nominal equality.
    412 
    ---     See Note [Decomposing AppTy equalities]
    413 
    -can_eq_nc True _rdr_env _envs ev NomEq ty1 _ ty2 _
    414 
    -  | Just (t1, s1) <- tcSplitAppTy_maybe ty1
    436 
    +-- Decompose applications
    437 
    +can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
    438 
    +  | True <- rewritten -- Why True?  See Note [Canonicalising type applications]
    439 
    +  -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
    440 
    +  , Just (t1, s1) <- tcSplitAppTy_maybe ty1
    415 441 
       , Just (t2, s2) <- tcSplitAppTy_maybe ty2
    416 
    -  = can_eq_app ev t1 s1 t2 s2
    442 
    +  = case eq_rel of
    443 
    +       NomEq  -> can_eq_app ev t1 s1 t2 s2
    444 
    +                 -- Only decompose AppTy for nominal equality.
    445 
    +                 -- See (APT1) in Note [Decomposing AppTy equalities]
    446 
    +
    447 
    +       ReprEq | ty1 `tcEqType` ty2 -> canEqReflexive ev ReprEq ty1
    448 
    +                 -- tcEqType: see (APT2) in Note [Decomposing AppTy equalities]
    449 
    +              | otherwise          -> finishCanWithIrred ReprEqReason ev
    417 450
    418 451 
     -------------------
    419 452 
     -- Can't decompose.
    ... ... @@ -665,124 +698,18 @@ There are lots of wrinkles of course:
    665 698 
        the attempt if we fail.
    666 699 
     -}
    667 700
    668 
    -{- Note [Unwrap newtypes first]
    669 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    670 
    -See also Note [Decomposing newtype equalities]
    671 
    -
    672 
    -Consider
    673 
    -  newtype N m a = MkN (m a)
    674 
    -N will get a conservative, Nominal role for its second parameter 'a',
    675 
    -because it appears as an argument to the unknown 'm'. Now consider
    676 
    -  [W] N Maybe a  ~R#  N Maybe b
    677 
    -
    678 
    -If we /decompose/, we'll get
    679 
    -  [W] a ~N# b
    680 
    -
    681 
    -But if instead we /unwrap/ we'll get
    682 
    -  [W] Maybe a ~R# Maybe b
    683 
    -which in turn gives us
    684 
    -  [W] a ~R# b
    685 
    -which is easier to satisfy.
    686 
    -
    687 
    -Conclusion: we must unwrap newtypes before decomposing them. This happens
    688 
    -in `can_eq_newtype_nc`
    689 
    -
    690 
    -We did flirt with making the /rewriter/ expand newtypes, rather than
    691 
    -doing it in `can_eq_newtype_nc`.   But with recursive newtypes we want
    692 
    -to be super-careful about expanding!
    693 
    -
    694 
    -   newtype A = MkA [A]   -- Recursive!
    695 
    -
    696 
    -   f :: A -> [A]
    697 
    -   f = coerce
    698 
    -
    699 
    -We have [W] A ~R# [A].  If we rewrite [A], it'll expand to
    700 
    -   [[[[[...]]]]]
    701 
    -and blow the reduction stack.  See Note [Newtypes can blow the stack]
    702 
    -in GHC.Tc.Solver.Rewrite.  But if we expand only the /top level/ of
    703 
    -both sides, we get
    704 
    -   [W] [A] ~R# [A]
    705 
    -which we can, just, solve by reflexivity.
    706 
    -
    707 
    -So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`.
    708 
    -
    709 
    -This is all very delicate. There is a real risk of a loop in the type checker
    710 
    -with recursive newtypes -- but I think we're doomed to do *something*
    711 
    -delicate, as we're really trying to solve for equirecursive type
    712 
    -equality. Bottom line for users: recursive newtypes do not play well with type
    713 
    -inference for representational equality.  See also Section 5.3.1 and 5.3.4 of
    714 
    -"Safe Zero-cost Coercions for Haskell" (JFP 2016).
    715 
    -
    716 
    -See also Note [Decomposing newtype equalities].
    717 
    -
    718 
    ---- Historical side note ---
    719 
    -
    720 
    -We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply;
    721 
    -see #22519.  But that didn't work: see discussion in #22924. Specifically
    722 
    -we got a loop with a minor variation:
    723 
    -   f2 :: a -> [A]
    724 
    -   f2 = coerce
    725 
    -
    726 
    -Note [Eager reflexivity check]
    727 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    728 
    -Suppose we have
    729 
    -
    730 
    -  newtype X = MkX (Int -> X)
    731 
    -
    732 
    -and
    733 
    -
    734 
    -  [W] X ~R X
    735 
    -
    736 
    -Naively, we would start unwrapping X and end up in a loop. Instead,
    737 
    -we do this eager reflexivity check. This is necessary only for representational
    738 
    -equality because the rewriter technology deals with the similar case
    739 
    -(recursive type families) for nominal equality.
    740 
    -
    741 
    -Note that this check does not catch all cases, but it will catch the cases
    742 
    -we're most worried about, types like X above that are actually inhabited.
    743 
    -
    744 
    -Here's another place where this reflexivity check is key:
    745 
    -Consider trying to prove (f a) ~R (f a). The AppTys in there can't
    746 
    -be decomposed, because representational equality isn't congruent with respect
    747 
    -to AppTy. So, when canonicalising the equality above, we get stuck and
    748 
    -would normally produce a CIrredCan. However, we really do want to
    749 
    -be able to solve (f a) ~R (f a). So, in the representational case only,
    750 
    -we do a reflexivity check.
    751 
    -
    752 
    -(This would be sound in the nominal case, but unnecessary, and I [Richard
    753 
    -E.] am worried that it would slow down the common case.)
    754 
    -
    755 
    - Note [Newtypes can blow the stack]
    756 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    757 
    -Suppose we have
    758 
    -
    759 
    -  newtype X = MkX (Int -> X)
    760 
    -  newtype Y = MkY (Int -> Y)
    761 
    -
    762 
    -and now wish to prove
    763 
    -
    764 
    -  [W] X ~R Y
    765 
    -
    766 
    -This Wanted will loop, expanding out the newtypes ever deeper looking
    767 
    -for a solid match or a solid discrepancy. Indeed, there is something
    768 
    -appropriate to this looping, because X and Y *do* have the same representation,
    769 
    -in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
    770 
    -coercion will ever witness it. This loop won't actually cause GHC to hang,
    771 
    -though, because we check our depth in `can_eq_newtype_nc`.
    772 
    --}
    773 
    -
    774 701 
     ------------------------
    775 702 
     -- | We're able to unwrap a newtype. Update the bits accordingly.
    776 703 
     can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs
    777 704 
                       -> CtEvidence           -- ^ :: ty1 ~ ty2
    778 705 
                       -> SwapFlag
    779 
    -                  -> ((Bag GlobalRdrElt, TcCoercion), TcType)  -- ^ :: ty1 ~ ty1'
    706 
    +                  -> (GlobalRdrElt, TcCoercion, TcType)  -- ^ :: ty1 ~ ty1'
    780 707 
                       -> TcType               -- ^ ty2
    781 708 
                       -> TcType               -- ^ ty2, with type synonyms
    782 709 
                       -> TcS (StopOrContinue (Either IrredCt EqCt))
    783 
    -can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2
    710 
    +can_eq_newtype_nc rdr_env envs ev swapped (gre, co1, ty1') ty2 ps_ty2
    784 711 
       = do { traceTcS "can_eq_newtype_nc" $
    785 
    -         vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
    712 
    +         vcat [ ppr ev, ppr swapped, ppr co1, ppr gre, ppr ty1', ppr ty2 ]
    786 713
    787 714 
              -- Check for blowing our stack, and increase the depth
    788 715 
              -- See Note [Newtypes can blow the stack]
    ... ... @@ -791,14 +718,20 @@ can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2
    791 718
    792 719 
              -- Next, we record uses of newtype constructors, since coercing
    793 720 
              -- through newtypes is tantamount to using their constructors.
    794 
    -       ; recordUsedGREs gres
    721 
    +       ; recordUsedGRE gre
    795 722
    796 723 
            ; let redn1 = mkReduction co1 ty1'
    797 724 
                  redn2 = mkReflRedn Representational ps_ty2
    798 
    -       ; new_ev <- rewriteEqEvidence ev' swapped redn1 redn2
    725 
    +       ; new_ev <- rewriteEqEvidence ev' (flipSwap swapped) redn2 redn1
    799 726 
                                          emptyCoHoleSet
    800 727
    801 
    -       ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
    728 
    +       -- ty1 is the one being unwrapped. Loop back to can_eq_nc with
    729 
    +       -- the arguments flipped so that ty2 is looked at first in the
    730 
    +       -- next iteration.  That way if we have (Id Rec) ~R# (Id Rec)
    731 
    +       -- where newtype Id a = MkId a  and newtype Rec = MkRec Rec
    732 
    +       -- we'll unwrap both Ids, then spot Rec=Rec.
    733 
    +       -- See (END2) in Note [Eager newtype decomposition]
    734 
    +       ; can_eq_nc False rdr_env envs new_ev ReprEq ty2 ps_ty2 ty1' ty1' }
    802 735
    803 736 
     ---------
    804 737 
     -- ^ Decompose a type application.
    ... ... @@ -896,7 +829,7 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2)
    896 829 
       | tc1 == tc2
    897 830 
       , tys1 `equalLength` tys2
    898 831 
       = do { inerts <- getInertSet
    899 
    -       ; if can_decompose inerts
    832 
    +       ; if canDecomposeTcApp ev eq_rel tc1 inerts
    900 833 
              then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2)
    901 834 
              else assert (eq_rel == ReprEq) $
    902 835 
                   canEqSoftFailure ReprEqReason ev ty1 ty2 }
    ... ... @@ -918,19 +851,31 @@ canTyConApp ev eq_rel both_generative (ty1,tc1,tys1) (ty2,tc2,tys2)
    918 851
    919 852 
       | otherwise
    920 853 
       = canEqSoftFailure ReprEqReason ev ty1 ty2
    921 
    -  where
    854 
    +
    855 
    +canDecomposeTcApp :: CtEvidence -> EqRel -> TyCon -> InertSet -> Bool
    922 856 
          -- See Note [Decomposing TyConApp equalities]
    923 857 
          -- and Note [Decomposing newtype equalities]
    924 
    -    can_decompose inerts
    925 
    -      =  isInjectiveTyCon tc1 (eqRelRole eq_rel)
    926 
    -      || (assert (eq_rel == ReprEq) $
    927 
    -          -- assert: isInjectiveTyCon is always True for Nominal except
    928 
    -          --   for type synonyms/families, neither of which happen here
    929 
    -          -- Moreover isInjectiveTyCon is True for Representational
    930 
    -          --   for algebraic data types.  So we are down to newtypes
    931 
    -          --   and data families.
    932 
    -          ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts)
    933 
    -             -- See Note [Decomposing newtype equalities] (EX2)
    858 
    +canDecomposeTcApp ev eq_rel tc inerts
    859 
    +  | isInjectiveTyCon tc eq_role = True
    860 
    +  | isGiven ev                  = False
    861 
    +  | otherwise                   = assert (eq_rel == ReprEq) $
    862 
    +                                  assert (isNewTyCon tc ||
    863 
    +                                          isDataFamilyTyCon tc ||
    864 
    +                                          isAbstractTyCon tc ) $
    865 
    +                                  noGivenNewtypeReprEqs tc inerts
    866 
    +    -- The otherwise case deals with
    867 
    +    --    * Representational equalities (T s1..sn) ~R# (T t1..tn)
    868 
    +    --    * where T is a newtype or data family or abstract
    869 
    +    -- Why? isInjectiveTyCon is always True for eq_rel=NomEq except for type
    870 
    +    --   synonyms/families, neither of which happen here; and isInjectiveTyCon
    871 
    +    --   is True for Representational for algebraic data types.
    872 
    +    --
    873 
    +    -- noGivenNewtypeReprEqs: see Note [Decomposing newtype equalities] (EX4)
    874 
    +    --    Decomposing here is a last resort
    875 
    +    -- NB: despite all these tests, decomposition of data familiies is alas
    876 
    +    --     /still/ incomplete. See (EX3) in Note [Decomposing newtype equalities]
    877 
    +  where
    878 
    +    eq_role = eqRelRole eq_rel
    934 879
    935 880 
     {- Note [Canonicalising TyCon/TyCon equalities]
    936 881 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -945,7 +890,7 @@ Suppose we are canonicalising [W] Int ~R# DF (TF a). Then
    945 890 
     (TC1) We might have an inert Given (a ~# Char), so if we rewrote the wanted
    946 891 
           (i.e. went around again in `can_eq_nc` with `rewritten`=True, we'd get
    947 892 
              [W] Int ~R# DF Bool
    948 
    -      and then the `tcTopNormaliseNewTypeTF_maybe` call would fire and
    893 
    +      and then the `tcUnwrapNewtype_maybe` call would fire and
    949 894 
           we'd unwrap the newtype.  So we must do that "go round again" bit.
    950 895 
           Hence the complicated guard (rewritten || both_generative) in `can_eq_nc`.
    951 896
    ... ... @@ -1114,6 +1059,110 @@ This is not a very big deal. It reduces the number of solver steps
    1114 1059 
     in the test RaeJobTalk from 1830 to 1815, a 1% reduction.  But still,
    1115 1060 
     it doesn't cost anything either.
    1116 1061
    1062 
    +Note [Solving newtype equalities: overview]
    1063 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1064 
    +This Note also applies to data families, which we treat like
    1065 
    +newtype in case of 'newtype instance'.
    1066 
    +
    1067 
    +Consider (N s1..sn) ~R#  (N t1..tn), where N is a newtype.
    1068 
    +We try three strategies, in order:
    1069 
    +
    1070 
    +(NTE1) Decompose if the si/ti are either (a) identical or (b) phantom. This step
    1071 
    +   avoids unwrapping, which allows success in some cases where the newtype
    1072 
    +   would unwrap infinitely. See Note [Eager newtype decomposition]
    1073 
    +
    1074 
    +(NTE2) Unwrap the newtype, if possible.  Always good, but it requires the data
    1075 
    +   constructor to be in scope.  See Note [Unwrap newtypes first].
    1076 
    +
    1077 
    +   If the newtype is recursive, this unwrapping might go on forever,
    1078 
    +   so `can_eq_newtype_nc` has a depth bound check.
    1079 
    +   See Note [Newtypes can blow the stack]
    1080 
    +
    1081 
    +(NTE3) Decompose the tycon application.  This step is a last resort, because it
    1082 
    +   risks losing completeness. See Note [Decomposing newtype equalities]
    1083 
    +
    1084 
    +Note [Newtypes can blow the stack]
    1085 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1086 
    +Suppose we have
    1087 
    +
    1088 
    +  newtype X = MkX (Int -> X)
    1089 
    +  newtype Y = MkY (Int -> Y)
    1090 
    +
    1091 
    +and now wish to prove
    1092 
    +
    1093 
    +  [W] X ~R Y
    1094 
    +
    1095 
    +This Wanted will loop, expanding out the newtypes ever deeper looking
    1096 
    +for a solid match or a solid discrepancy. Indeed, there is something
    1097 
    +appropriate to this looping, because X and Y *do* have the same representation,
    1098 
    +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
    1099 
    +coercion will ever witness it. This loop won't actually cause GHC to hang,
    1100 
    +though, because we check our depth in `can_eq_newtype_nc`.
    1101 
    +
    1102 
    +However, GHC can still loop badly: see #26757, which shows how we can create
    1103 
    +types whose size is exponential in the depth of newtype expansion. That makes
    1104 
    +GHC go out to lunch unless the depth bound is very small indeed; and a small
    1105 
    +depth bound makes perfectly legitimate programs fail.  We don't have solid
    1106 
    +solution for this, but it's rare.
    1107 
    +
    1108 
    +Note [Unwrap newtypes first]
    1109 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1110 
    +See also Note [Decomposing newtype equalities]
    1111 
    +
    1112 
    +Consider
    1113 
    +  newtype N m a = MkN (m a)
    1114 
    +N will get a conservative, Nominal role for its second parameter 'a',
    1115 
    +because it appears as an argument to the unknown 'm'. Now consider
    1116 
    +  [W] N Maybe a  ~R#  N Maybe b
    1117 
    +
    1118 
    +If we /decompose/, we'll get
    1119 
    +  [W] a ~N# b
    1120 
    +
    1121 
    +But if instead we /unwrap/ we'll get
    1122 
    +  [W] Maybe a ~R# Maybe b
    1123 
    +which in turn gives us
    1124 
    +  [W] a ~R# b
    1125 
    +which is easier to satisfy.
    1126 
    +
    1127 
    +Conclusion: we must unwrap newtypes before decomposing them. This happens
    1128 
    +in `can_eq_newtype_nc`
    1129 
    +
    1130 
    +We did flirt with making the /rewriter/ expand newtypes, rather than
    1131 
    +doing it in `can_eq_newtype_nc`.   But with recursive newtypes we want
    1132 
    +to be super-careful about expanding!
    1133 
    +
    1134 
    +   newtype A = MkA [A]   -- Recursive!
    1135 
    +
    1136 
    +   f :: A -> [A]
    1137 
    +   f = coerce
    1138 
    +
    1139 
    +We have [W] A ~R# [A].  If we rewrite [A], it'll expand to
    1140 
    +   [[[[[...]]]]]
    1141 
    +and blow the reduction stack.  See Note [Newtypes can blow the stack]
    1142 
    +in GHC.Tc.Solver.Rewrite.  But if we expand only the /top level/ of
    1143 
    +both sides, we get
    1144 
    +   [W] [A] ~R# [A]
    1145 
    +which we can, just, solve by reflexivity.
    1146 
    +
    1147 
    +So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`.
    1148 
    +
    1149 
    +This is all very delicate. There is a real risk of a loop in the type checker
    1150 
    +with recursive newtypes -- but I think we're doomed to do *something*
    1151 
    +delicate, as we're really trying to solve for equirecursive type
    1152 
    +equality. Bottom line for users: recursive newtypes do not play well with type
    1153 
    +inference for representational equality.  See also Section 5.3.1 and 5.3.4 of
    1154 
    +"Safe Zero-cost Coercions for Haskell" (JFP 2016).
    1155 
    +
    1156 
    +See also Note [Decomposing newtype equalities].
    1157 
    +
    1158 
    +--- Historical side note ---
    1159 
    +
    1160 
    +We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply;
    1161 
    +see #22519.  But that didn't work: see discussion in #22924. Specifically
    1162 
    +we got a loop with a minor variation:
    1163 
    +   f2 :: a -> [A]
    1164 
    +   f2 = coerce
    1165 
    +
    1117 1166 
     Note [Decomposing newtype equalities]
    1118 1167 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1119 1168 
     This Note also applies to data families, which we treat like
    ... ... @@ -1133,7 +1182,10 @@ if the newtype is abstract (so can't be unwrapped) we can only solve
    1133 1182 
     the equality by (a) using a Given or (b) decomposition.  If (a) is impossible
    1134 1183 
     (e.g. no Givens) then (b) is safe albeit potentially incomplete.
    1135 1184
    1136 
    -There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1185 
    +Remember: Decomposing Wanteds is always /sound/.
    1186 
    +          This Note is only about /completeness/.
    1187 
    +
    1188 
    +There are three ways in which decomposing [W] (N ty1) ~r (N ty2) could be incomplete:
    1137 1189
    1138 1190 
     * Incompleteness example (EX1): unwrap first
    1139 1191 
           newtype Nt a = MkNt (Id a)
    ... ... @@ -1146,7 +1198,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1146 1198 
       which is unsatisfiable. Unwrapping, though, leads to a solution.
    1147 1199
    1148 1200 
       CONCLUSION: always unwrap newtypes before attempting to decompose
    1149 
    -  them.  This is done in can_eq_nc.  Of course, we can't unwrap if the data
    1201 
    +  them.  This is done in `can_eq_nc`.  Of course, we can't unwrap if the data
    1150 1202 
       constructor isn't in scope.  See Note [Unwrap newtypes first].
    1151 1203
    1152 1204 
     * Incompleteness example (EX2): prioritise Nominal equalities. See #24887
    ... ... @@ -1154,20 +1206,32 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1154 1206 
           data instance D Int  = MkD1 (D Char)
    1155 1207 
           data instance D Bool = MkD2 (D Char)
    1156 1208 
       Now suppose we have
    1157 
    -      [W] g1: D Int ~R# D a
    1158 
    -      [W] g2: a ~# Bool
    1159 
    -  If we solve g2 first, giving a:=Bool, then we can solve g1 easily:
    1209 
    +      [W] g1: D Int ~R# D alpha
    1210 
    +      [W] g2: alpha ~# Bool
    1211 
    +  If we solve g2 first, giving alpha:=Bool, then we can solve g1 easily:
    1160 1212 
           D Int ~R# D Char ~R# D Bool
    1161 1213 
       by newtype unwrapping.
    1162 1214
    1163 1215 
       BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only)
    1164 
    -  leaving     [W] D Char ~#R D Bool
    1165 
    -  If we decompose now, we'll get (Char ~R# Bool), which is insoluble.
    1216 
    +  leaving     [W] D Char ~#R D alpha
    1217 
    +  If we decompose now, we'll get (Char ~R# alpha), which is insoluble, since
    1218 
    +  alpha turns out to be Bool.
    1166 1219
    1167 1220 
       CONCLUSION: prioritise nominal equalites in the work list.
    1168 1221 
       See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet.
    1169 1222
    1170 
    -* Incompleteness example (EX3): check available Givens
    1223 
    +* Incompleteness example (EX3)
    1224 
    +  Sadly, the fix for (EX2) is /still/ incomplete:
    1225 
    +     * The equality `g2` might be in a sibling implication constraint,
    1226 
    +       invisible for now.
    1227 
    +     * The equality `g2` might be hidden in a class constraint:
    1228 
    +          class C a
    1229 
    +          instance (a~Bool) => C [a]
    1230 
    +          [W] g3 :: C [alpha]
    1231 
    +       When we get around to solving `g3` we'll discover (g2:alpha~Bool)
    1232 
    +  So that's a real infelicity in the solver.
    1233 
    +
    1234 
    +* Incompleteness example (EX4): check available Givens
    1171 1235 
           newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
    1172 1236 
           type role Nt representational  -- but the user gives it an R role anyway
    1173 1237
    ... ... @@ -1230,18 +1294,48 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1230 1294 
       un-expanded equality superclasses; but only in some very obscure
    1231 1295 
       recursive-superclass situations.
    1232 1296
    1233 
    -   Yet another approach (!) is described in
    1234 
    -   Note [Decomposing newtypes a bit more aggressively].
    1235 
    -
    1236 
    -Remember: decomposing Wanteds is always /sound/. This Note is
    1237 
    -only about /completeness/.
    1238 
    -
    1239 
    -Note [Decomposing newtypes a bit more aggressively]
    1240 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1241 
    -IMPORTANT: the ideas in this Note are *not* implemented. Instead, the
    1242 
    -current approach is detailed in Note [Decomposing newtype equalities]
    1243 
    -and Note [Unwrap newtypes first].
    1244 
    -For more details about the ideas in this Note see
    1297 
    +Note [Eager newtype decomposition]
    1298 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1299 
    +Consider [W] (Rec1 Int) ~R#  (Rec1 Bool) where
    1300 
    +  newtype Rec1 a = MkRec1 (Rec1 a)
    1301 
    +
    1302 
    +If we apply (NTE2), we'll loop because `Rec1` unwraps forever.
    1303 
    +But the role of `a` is inferred as Phantom, so it sound and complete
    1304 
    +to decompose via `canDecomposableTyConAppOK`, giving nothing at all
    1305 
    +(because of the Phantom role).  So we win.
    1306 
    +
    1307 
    +Another useful special case is
    1308 
    +   newtype Rec = MkRec Rec
    1309 
    +where there are no arguments.
    1310 
    +
    1311 
    +So we do an eager decomposition check in step (NTE1), /before/ trying to unwrap
    1312 
    +in (NTE2).  This is a HACK: it catches some cases of recursion, but not all.
    1313 
    +But it's a hack that has been in GHC for some time.
    1314 
    +
    1315 
    +Wrinkles
    1316 
    +
    1317 
    +(END1) The eager-decomposition step is fine for all data types, not just newtypes.
    1318 
    +
    1319 
    +(END2) Consider    newtype Id a = MkId a      -- Not recusrive
    1320 
    +                   newtype Rec  = MkRec Rec   -- Recursive
    1321 
    +  and [W] Id Rec ~R#  Rec
    1322 
    +  Then (NTE1) will fail; (NTE2) will succeed in unwrapping Id, generating
    1323 
    +  [W] Rec ~R# Rec; and (NTE1) will succeed when we go round the loop.
    1324 
    +
    1325 
    +  What about [W] Rec ~R# Id Rec?
    1326 
    +  Here (NTE1) will fail again; (NTE2) will succeed, by unwrapping Rec, to get
    1327 
    +  Rec again.  If we just iterate with [W] Rec ~R# Id Rec, we'll be stuck in
    1328 
    +  a loop.  Instead we want to flip the constraint round so we get
    1329 
    +  [W] Id Rec ~R# Rec.  Now we win.  See the flipping in `can_eq_newtype_nc`.
    1330 
    +
    1331 
    +(END3) See Note [Even more eager newtype decomposition]
    1332 
    +
    1333 
    +Note [Even more eager newtype decomposition]
    1334 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1335 
    +Note [Eager newtype decomposition] decomposes [W] (N s ~R# N t) if N's role is
    1336 
    +phantom.  We could go further and decompose if the arguments are all Phantom
    1337 
    +/or/ Representational. This is not implemented.  For more details about the
    1338 
    +ideas in this Note see
    1245 1339 
       * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549
    1246 1340 
       * issue #22441
    1247 1341 
       * discussion on !9282.
    ... ... @@ -1249,9 +1343,8 @@ For more details about the ideas in this Note see
    1249 1343 
     Consider [G] c, [W] (IO Int) ~R (IO Age)
    1250 1344 
     where IO is abstract, and
    1251 1345 
        newtype Age = MkAge Int   -- Not abstract
    1252 
    -With the above rules, if there any Given Irreds,
    1253 
    -the Wanted is insoluble because we can't decompose it.  But in fact,
    1254 
    -if we look at the defn of IO, roughly,
    1346 
    +With the above rules, if there any Given Irreds, the Wanted is insoluble because
    1347 
    +we can't decompose it.  But in fact, if we look at the defn of IO, roughly,
    1255 1348 
         newtype IO a = State# -> (State#, a)
    1256 1349 
     we can see that decomposing [W] (IO Int) ~R (IO Age) to
    1257 1350 
         [W] Int ~R Age
    ... ... @@ -1260,41 +1353,26 @@ IO's argment is representational. Hence:
    1260 1353
    1261 1354 
       DecomposeNewtypeIdea:
    1262 1355 
          decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
    1263 
    -     if the roles of all N's arguments are representational
    1264 
    -
    1265 
    -If N's arguments really /are/ representational this will not lose
    1266 
    -completeness.  Here "really are representational" means "if you expand
    1267 
    -all newtypes in N's RHS, we'd infer a representational role for each
    1268 
    -of N's type variables in that expansion".  See Note [Role inference]
    1269 
    -in GHC.Tc.TyCl.Utils.
    1270 
    -
    1271 
    -But the user might /override/ a phantom role with an explicit role
    1272 
    -annotation, and then we could (obscurely) get incompleteness.
    1273 
    -Consider
    1274 
    -
    1275 
    -   module A( silly, T ) where
    1276 
    -     newtype T a = MkT Int
    1277 
    -     type role T representational  -- Override phantom role
    1278 
    -
    1279 
    -     silly :: Coercion (T Int) (T Bool)
    1280 
    -     silly = Coercion  -- Typechecks by unwrapping the newtype
    1356 
    +     if the roles of all N's arguments are representational (or phantom)
    1281 1357
    1282 
    -     data Coercion a b where  -- Actually defined in Data.Type.Coercion
    1283 
    -       Coercion :: Coercible a b => Coercion a b
    1358 
    +If N's arguments really /are/ representational this will not lose completeness.
    1359 
    +Here "really are representational" means "if you expand all newtypes in N's RHS,
    1360 
    +we'd infer a representational role for each of N's type variables in that
    1361 
    +expansion".  See Note [Role inference] in GHC.Tc.TyCl.Utils.
    1284 1362
    1285 
    -   module B where
    1286 
    -     import A
    1287 
    -     f :: T Int -> T Bool
    1288 
    -     f = case silly of Coercion -> coerce
    1363 
    +But the user might /override/ a phantom role with an explicit role annotation,
    1364 
    +and then we could (obscurely) get incompleteness.  Consider (#9117):
    1365 
    +   newtype Phant a = MkPhant Char
    1366 
    +   type role Phant representational  -- Override phantom role
    1367 
    +   [W] Phant Int ~R# Phant Char
    1289 1368
    1290 
    -Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose,
    1291 
    -we'll get stuck with (Int ~R Bool).  Instead we want to use the
    1292 
    -[G] (T Int) ~R (T Bool), which will be in the Irreds.
    1369 
    +We do not want to decompose to Int ~R# Char; better to unwrap
    1293 1370
    1294 1371 
     Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very
    1295 1372 
     obscure incompleteness (above).  But no one is reporting a problem from
    1296 1373 
     the lack of decompostion, so we'll just leave it for now.  This long
    1297 1374 
     Note is just to record the thinking for our future selves.
    1375 
    +---- End of speculative aside ---------
    1298 1376
    1299 1377 
     Note [Decomposing AppTy equalities]
    1300 1378 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -1305,12 +1383,12 @@ Note [Decomposing TyConApp equalities]. We have
    1305 1383 
         s1 t1 ~N s2 t2        ==>   s1 ~N s2,  t1 ~N t2  (CO_LEFT, CO_RIGHT)
    1306 1384
    1307 1385 
     In the first of these, why do we need Nominal equality in (t1 ~N t2)?
    1308 
    -See {2} below.
    1386 
    +See (APT3) below.
    1309 1387
    1310 1388 
     For sound and complete solving, we need both directions to decompose. So:
    1311 1389 
     * At nominal role, all is well: we have both directions.
    1312 
    -* At representational role, decomposition of Givens is unsound (see {1} below),
    1313 
    -  and decomposition of Wanteds is incomplete.
    1390 
    +* At representational role, decomposition of Givens is unsound
    1391 
    +  (see (APT1) below), and decomposition of Wanteds is incomplete.
    1314 1392
    1315 1393 
     Here is an example of the incompleteness for Wanteds:
    1316 1394
    ... ... @@ -1325,7 +1403,7 @@ Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get
    1325 1403 
         [W] w4 :: b ~N a
    1326 1404
    1327 1405 
     Note that w4 is *nominal*. A nominal role here is necessary because AppCo
    1328 
    -requires a nominal role on its second argument. (See {2} for an example of
    1406 
    +requires a nominal role on its second argument. (See (APT3) for an example of
    1329 1407 
     why.) Now we are stuck, because w4 is insoluble. On the other hand, if we
    1330 1408 
     see w2 first, setting alpha := Maybe, all is well, as we can decompose
    1331 1409 
     Maybe b ~R Maybe a into b ~R a.
    ... ... @@ -1348,12 +1426,21 @@ Bottom line:
    1348 1426 
       the lack of an equation in can_eq_nc
    1349 1427
    1350 1428 
     Extra points
    1351 
    -{1}  Decomposing a Given AppTy over a representational role is simply
    1429 
    +(APT1) Decomposing a Given AppTy at Representational role is simply
    1352 1430 
          unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
    1353 1431 
          the newtype Phant, above), then we surely don't want any relationship
    1354 1432 
          between Int and Bool, lest we also have co2 :: Phant ~ a around.
    1355 1433
    1356 
    -{2} The role on the AppCo coercion is a conservative choice, because we don't
    1434 
    +     For Wanteds, decomposing an AppTy at Representational role is incomplete.
    1435 
    +
    1436 
    +(APT2) What if we have  [W]  (f a) ~R# (f a)
    1437 
    +   We can't decompose because of (APT1).  But it's silly to reject.  So we do
    1438 
    +   an equality check, in the AppTy/AppTy case of `can_eq_nc`.
    1439 
    +
    1440 
    +   (It would be sound to do this reflexivity check in the Nominal case too,
    1441 
    +   but not necessary, and there might be a perf cost.)
    1442 
    +
    1443 
    +(APT3) The role on the AppCo coercion is a conservative choice, because we don't
    1357 1444 
         know the role signature of the function. For example, let's assume we could
    1358 1445 
         have a representational role on the second argument of AppCo. Then, consider
    1359 1446

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -22,7 +22,7 @@ module GHC.Tc.Solver.Monad (
    22 22 
         updWorkListTcS,
    23 23 
         pushLevelNoWorkList, pushTcLevelM_,
    24 24
    25 
    -    runTcPluginTcS, recordUsedGREs,
    25 
    +    runTcPluginTcS, recordUsedGRE,
    26 26 
         matchGlobalInst, TcM.ClsInstResult(..),
    27 27
    28 28 
         QCInst(..),
    ... ... @@ -1519,18 +1519,16 @@ tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n
    1519 1519 
     -- pure veneer of TcS. But it's just about warnings around unused imports
    1520 1520 
     -- and local constructors (GHC will issue fewer warnings than it otherwise
    1521 1521 
     -- might), so it's not worth losing sleep over.
    1522 
    -recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
    1523 
    -recordUsedGREs gres
    1524 
    -  = do { wrapTcS $ TcM.addUsedGREs NoDeprecationWarnings gre_list
    1522 
    +recordUsedGRE :: GlobalRdrElt -> TcS ()
    1523 
    +recordUsedGRE gre
    1524 
    +  = do { wrapTcS $ TcM.addUsedGRE NoDeprecationWarnings gre
    1525 1525 
              -- If a newtype constructor was imported, don't warn about not
    1526 1526 
              -- importing it...
    1527 
    -       ; wrapTcS $ traverse_ (TcM.keepAlive . greName) gre_list }
    1527 
    +       ; wrapTcS $ TcM.keepAlive (greName gre) }
    1528 1528 
              -- ...and similarly, if a newtype constructor was defined in the same
    1529 1529 
              -- module, don't warn about it being unused.
    1530 1530 
              -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
    1531 1531
    1532 
    -  where
    1533 
    -    gre_list = bagToList gres
    1534 1532
    1535 1533 
     -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
    1536 1534 
     -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  • testsuite/tests/deriving/should_fail/T8984.stderr
    1 1 
     T8984.hs:7:46: error: [GHC-18872]
    2 
    -    • Couldn't match representation of type: cat a (N cat a Int)
    3 
    -                               with that of: cat a (cat a Int)
    2 
    +    • Couldn't match representation of type: cat a (cat a Int)
    3 
    +                               with that of: cat a (N cat a Int)
    4 4 
             arising from the coercion of the method ‘app’
    5 5 
               from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’
    6 6 
           Note: We cannot know what roles the parameters to ‘cat a’ have;

  • testsuite/tests/deriving/should_fail/deriving-via-fail.stderr
    1 1 
     deriving-via-fail.hs:10:34: error: [GHC-10283]
    2 
    -    • Couldn't match representation of type ‘a’ with that of ‘b’
    2 
    +    • Couldn't match representation of type ‘b’ with that of ‘a’
    3 3 
             arising from the coercion of the method ‘showsPrec’
    4 4 
               from type ‘Int -> Identity b -> ShowS’
    5 5 
                 to type ‘Int -> Foo1 a -> ShowS’
    6 
    -      ‘a’ is a rigid type variable bound by
    6 
    +      ‘b’ is a rigid type variable bound by
    7 7 
             the deriving clause for ‘Show (Foo1 a)’
    8 8 
             at deriving-via-fail.hs:10:34-37
    9 
    -      ‘b’ is a rigid type variable bound by
    9 
    +      ‘a’ is a rigid type variable bound by
    10 10 
             the deriving clause for ‘Show (Foo1 a)’
    11 11 
             at deriving-via-fail.hs:10:34-37
    12 12 
         • When deriving the instance for (Show (Foo1 a))

  • testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
    1 1 
     deriving-via-fail4.hs:15:12: error: [GHC-18872]
    2 
    -    • Couldn't match representation of type ‘Int’ with that of ‘Char’
    2 
    +    • Couldn't match representation of type ‘Char’ with that of ‘Int’
    3 3 
             arising from the coercion of the method ‘==’
    4 4 
               from type ‘Char -> Char -> Bool’ to type ‘F1 -> F1 -> Bool’
    5 5 
         • When deriving the instance for (Eq F1)
    6 6
    7 7 
     deriving-via-fail4.hs:18:13: error: [GHC-10283]
    8 
    -    • Couldn't match representation of type ‘a1’ with that of ‘a2’
    8 
    +    • Couldn't match representation of type ‘a2’ with that of ‘a1’
    9 9 
             arising from the coercion of the method ‘c’
    10 10 
               from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’
    11 
    -      ‘a1’ is a rigid type variable bound by
    11 
    +      ‘a2’ is a rigid type variable bound by
    12 12 
             the deriving clause for ‘C a (F2 a1)’
    13 13 
             at deriving-via-fail4.hs:18:13-15
    14 
    -      ‘a2’ is a rigid type variable bound by
    14 
    +      ‘a1’ is a rigid type variable bound by
    15 15 
             the deriving clause for ‘C a (F2 a1)’
    16 16 
             at deriving-via-fail4.hs:18:13-15
    17 17 
         • When deriving the instance for (C a (F2 a1))

  • testsuite/tests/deriving/should_fail/deriving-via-fail5.stderr
    1 1 
     deriving-via-fail5.hs:8:1: error: [GHC-10283]
    2 
    -    • Couldn't match representation of type ‘a’ with that of ‘b’
    2 
    +    • Couldn't match representation of type ‘b’ with that of ‘a’
    3 3 
             arising from a use of ‘GHC.Internal.Prim.coerce’
    4 
    -      ‘a’ is a rigid type variable bound by
    4 
    +      ‘b’ is a rigid type variable bound by
    5 5 
             the instance declaration
    6 6 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    7 
    -      ‘b’ is a rigid type variable bound by
    7 
    +      ‘a’ is a rigid type variable bound by
    8 8 
             the instance declaration
    9 9 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    10 10 
         • In the expression:
    ... ... @@ -25,12 +25,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283]
    25 25 
               (bound at deriving-via-fail5.hs:8:1)
    26 26
    27 27 
     deriving-via-fail5.hs:8:1: error: [GHC-10283]
    28 
    -    • Couldn't match representation of type ‘a’ with that of ‘b’
    28 
    +    • Couldn't match representation of type ‘b’ with that of ‘a’
    29 29 
             arising from a use of ‘GHC.Internal.Prim.coerce’
    30 
    -      ‘a’ is a rigid type variable bound by
    30 
    +      ‘b’ is a rigid type variable bound by
    31 31 
             the instance declaration
    32 32 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    33 
    -      ‘b’ is a rigid type variable bound by
    33 
    +      ‘a’ is a rigid type variable bound by
    34 34 
             the instance declaration
    35 35 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    36 36 
         • In the expression:
    ... ... @@ -48,12 +48,12 @@ deriving-via-fail5.hs:8:1: error: [GHC-10283]
    48 48 
             show :: Foo4 a -> String (bound at deriving-via-fail5.hs:8:1)
    49 49
    50 50 
     deriving-via-fail5.hs:8:1: error: [GHC-10283]
    51 
    -    • Couldn't match representation of type ‘a’ with that of ‘b’
    51 
    +    • Couldn't match representation of type ‘b’ with that of ‘a’
    52 52 
             arising from a use of ‘GHC.Internal.Prim.coerce’
    53 
    -      ‘a’ is a rigid type variable bound by
    53 
    +      ‘b’ is a rigid type variable bound by
    54 54 
             the instance declaration
    55 55 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    56 
    -      ‘b’ is a rigid type variable bound by
    56 
    +      ‘a’ is a rigid type variable bound by
    57 57 
             the instance declaration
    58 58 
             at deriving-via-fail5.hs:(8,1)-(9,24)
    59 59 
         • In the expression:

  • testsuite/tests/typecheck/should_compile/T26746.hs
    1 
    +module T26746 where
    2 
    +
    3 
    +import Data.Coerce
    4 
    +
    5 
    +newtype Foo a = Foo (Foo a)
    6 
    +newtype Age = MkAge Int
    7 
    +
    8 
    +ex1 :: (Foo Age) -> (Foo Int)
    9 
    +ex1 = coerce
    10 
    +
    11 
    +newtype Womble a = MkWomble (Foo a)
    12 
    +
    13 
    +ex2 :: Womble (Foo Age) -> (Foo Int)
    14 
    +ex2 = coerce
    15 
    +
    16 
    +ex3 :: (Foo Age) -> Womble (Foo Int)
    17 
    +ex3 = coerce
    18 
    +
    19 
    +
    20 
    +-- Surprisingly this one works:
    21 
    +newtype Z1 = MkZ1 Z2
    22 
    +newtype Z2 = MKZ2 Z1
    23 
    +
    24 
    +ex4 :: Z1 -> Z2
    25 
    +ex4 = coerce
    26 
    +
    27 
    +-- But this one does not (commented out)
    28 
    +-- newtype Y1 = MkY1 Y2
    29 
    +-- newtype Y2 = MKY2 Y3
    30 
    +-- newtype Y3 = MKY3 Y1
    31 
    +--
    32 
    +-- ex5 :: Y1 -> Y3
    33 
    +-- ex5 = coerce

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -957,3 +957,4 @@ test('T17705', normal, compile, [''])
    957 957 
     test('T14745', normal, compile, [''])
    958 958 
     test('T26451', normal, compile, [''])
    959 959 
     test('T26582', normal, compile, [''])
    960 
    +test('T26746', normal, compile, [''])

  • testsuite/tests/typecheck/should_fail/T15801.stderr
    1 1 
     T15801.hs:52:10: error: [GHC-18872]
    2 
    -    • Couldn't match representation of type: UnOp op_a -> UnOp b
    3 
    -                               with that of: op_a --> b
    4 
    -        arising (via a quantified constraint) from the superclasses of an instance declaration
    2 
    +    • Couldn't match representation of type: op_a --> b
    3 
    +                               with that of: UnOp op_a -> UnOp b
    4 
    +        arising (via a quantified constraint) from
    5 
    +          the superclasses of an instance declaration
    5 6 
           When trying to solve the quantified constraint
    6 7 
             forall (op_a :: Op (*)) (b :: Op (*)). op_a -#- b
    7 8 
             arising from the superclasses of an instance declaration

  • testsuite/tests/typecheck/should_fail/T22924b.stderr
    1 1 
     T22924b.hs:10:5: error: [GHC-40404]
    2 2 
         • Reduction stack overflow; size = 201
    3 
    -      When simplifying the following constraint: Coercible [R] S
    3 
    +      When simplifying the following constraint: Coercible S [R]
    4 4 
         • In the expression: coerce
    5 5 
           In an equation for ‘f’: f = coerce
    6 6 
         Suggested fix:

  • testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs
    ... ... @@ -20,15 +20,6 @@ foo4 = coerce $ one :: Down Int
    20 20 
     newtype Void = Void Void
    21 21 
     foo5 = coerce :: Void -> ()
    22 22
    23 
    -
    24 
    -------------------------------------
    25 
    --- This next one generates an exponentially big type as it
    26 
    --- tries to unwrap.  See comment:15 in #11518
    27 
    --- Adding assertions that force the types can make us
    28 
    --- run out of space.
    29 
    -newtype VoidBad a = VoidBad (VoidBad (a,a))
    30 
    -foo5' = coerce :: (VoidBad ()) -> ()
    31 
    -
    32 23 
     ------------------------------------
    33 24 
     -- This should fail with a context stack overflow
    34 25 
     newtype Fix f = Fix (f (Fix f))

  • testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
    ... ... @@ -34,23 +34,21 @@ TcCoercibleFail.hs:18:8: error: [GHC-18872]
    34 34 
           In the expression: coerce $ one :: Down Int
    35 35 
           In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int
    36 36
    37 
    -TcCoercibleFail.hs:21:8: error: [GHC-18872]
    38 
    -    • Couldn't match representation of type ‘Void’ with that of ‘()’
    39 
    -        arising from a use of ‘coerce’
    37 
    +TcCoercibleFail.hs:21:8: error: [GHC-40404]
    38 
    +    • Reduction stack overflow; size = 201
    39 
    +      When simplifying the following constraint: Coercible () Void
    40 40 
         • In the expression: coerce :: Void -> ()
    41 41 
           In an equation for ‘foo5’: foo5 = coerce :: Void -> ()
    42 
    +    Suggested fix:
    43 
    +      Use -freduction-depth=0 to disable this check
    44 
    +      (any upper bound you could choose might fail unpredictably with
    45 
    +       minor updates to GHC, so disabling the check is recommended if
    46 
    +       you're sure that type checking should terminate)
    42 47
    43 
    -TcCoercibleFail.hs:30:9: error: [GHC-18872]
    44 
    -    • Couldn't match representation of type ‘VoidBad ()’
    45 
    -                               with that of ‘()’
    46 
    -        arising from a use of ‘coerce’
    47 
    -    • In the expression: coerce :: (VoidBad ()) -> ()
    48 
    -      In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> ()
    49 
    -
    50 
    -TcCoercibleFail.hs:35:8: error: [GHC-40404]
    48 
    +TcCoercibleFail.hs:26:8: error: [GHC-40404]
    51 49 
         • Reduction stack overflow; size = 201
    52 50 
           When simplifying the following constraint:
    53 
    -        Coercible (Either Int (Fix (Either Int))) (Fix (Either Age))
    51 
    +        Coercible (Fix (Either Age)) (Either Int (Fix (Either Int)))
    54 52 
         • In the expression: coerce :: Fix (Either Int) -> Fix (Either Age)
    55 53 
           In an equation for ‘foo6’:
    56 54 
               foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)
    ... ... @@ -60,10 +58,9 @@ TcCoercibleFail.hs:35:8: error: [GHC-40404]
    60 58 
            minor updates to GHC, so disabling the check is recommended if
    61 59 
            you're sure that type checking should terminate)
    62 60
    63 
    -TcCoercibleFail.hs:36:8: error: [GHC-18872]
    64 
    -    • Couldn't match representation of type ‘Either
    65 
    -                                               Int (Fix (Either Int))’
    66 
    -                               with that of ‘()’
    61 
    +TcCoercibleFail.hs:27:8: error: [GHC-18872]
    62 
    +    • Couldn't match representation of type ‘()’
    63 
    +                               with that of ‘Either Int (Fix (Either Int))’
    67 64 
             arising from a use of ‘coerce’
    68 65 
         • In the expression: coerce :: Fix (Either Int) -> ()
    69 66 
           In an equation for ‘foo7’: foo7 = coerce :: Fix (Either Int) -> ()

  • testsuite/tests/typecheck/should_fail/all.T
    ... ... @@ -326,11 +326,7 @@ test('T7989', normal, compile_fail, [''])
    326 326 
     test('T8034', normal, compile_fail, [''])
    327 327 
     test('T8142', normal, compile_fail, [''])
    328 328 
     test('T8262', normal, compile_fail, [''])
    329 
    -
    330 
    -# TcCoercibleFail times out with the compiler is compiled with -DDEBUG.
    331 
    -# This is expected (see comment in source file).
    332 
    -test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, [''])
    333 
    -
    329 
    +test('TcCoercibleFail', [], compile_fail, [''])
    334 330 
     test('TcCoercibleFail2', [], compile_fail, [''])
    335 331 
     test('TcCoercibleFail3', [], compile_fail, [''])
    336 332 
     test('T8306', normal, compile_fail, [''])

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