Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC

Commits:

8 changed files:

Changes:

  • changelog.d/T27828
    ... ... @@ -4,5 +4,5 @@ issues: #27828
    4 4 
     mrs: !16714
    5 5
    6 6 
     description: {
    7 
    -    There was a bug in the implemenation of functional dependencies for type families.
    7 
    +    There was a bug in the implementation of functional dependencies for type families.
    8 8 
     }

  • compiler/GHC/Builtin/WiredIn/Types/Box.hs
    ... ... @@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty =
    329 329 
                             , cab_roles   = roles
    330 330 
                             , cab_lhs     = mkTyVarTys tvs
    331 331 
                             , cab_rhs     = nt_fld_ty
    332 
    -                        , cab_incomps = [] }
    332 
    +                        , cab_overlaps = []
    333 
    +                        , cab_incomps  = [] }
    333 334
    334 335 
     -- | The wired-in @Box@ newtype:
    335 336 
     --

  • compiler/GHC/Core/Coercion/Axiom.hs
    ... ... @@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom (
    18 18 
            coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
    19 19 
            coAxBranchRoles,
    20 20 
            coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
    21 
    -       placeHolderIncomps,
    21 
    +       placeHolderIncomps, placeHolderOverlaps,
    22 22
    23 23 
            Role(..),
    24 24
    ... ... @@ -275,8 +275,15 @@ data CoAxBranch
    275 275 
         , cab_rhs      :: Type
    276 276 
            -- ^ Right-hand side of the equality
    277 277 
            -- See Note [CoAxioms are homogeneous]
    278 
    +
    279 
    +    , cab_overlaps :: [CoAxBranch]
    280 
    +       -- ^ The preceding branches whose LHSs are /unify with/ this one
    281 
    +       -- Order is unimportant
    282 
    +       -- See Note [Storing compatibility]
    283 
    +
    278 284 
         , cab_incomps  :: [CoAxBranch]
    279 
    -       -- ^ The previous incompatible branches
    285 
    +       -- ^ The preceding branches that are /incompatible/ with this one
    286 
    +       -- Order is unimportant
    280 287 
            -- See Note [Storing compatibility]
    281 288 
         }
    282 289 
       deriving Data.Data
    ... ... @@ -349,8 +356,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
    349 356 
     coAxBranchIncomps = cab_incomps
    350 357
    351 358 
     -- See Note [Compatibility] in GHC.Core.FamInstEnv
    352 
    -placeHolderIncomps :: [CoAxBranch]
    353 
    -placeHolderIncomps = panic "placeHolderIncomps"
    359 
    +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch]
    360 
    +placeHolderIncomps  = panic "placeHolderIncomps"
    361 
    +placeHolderOverlaps = panic "placeHolderOverlaps"
    354 362
    355 363 
     {-
    356 364 
     Note [CoAxBranch type variables]

  • compiler/GHC/Core/FamInstEnv.hs
    ... ... @@ -487,22 +487,45 @@ in GHC.Core.Unify.)
    487 487
    488 488 
     Note [Compatibility]
    489 489 
     ~~~~~~~~~~~~~~~~~~~~
    490 
    -Two patterns are /compatible/ if either of the following conditions hold:
    490 
    +Consider a closed type family with two equations (X1) and (X2)
    491 
    +   type family F a where
    492 
    +      F lhs1 = rhs1   -- (X1)
    493 
    +      ...
    494 
    +      F lhs2 = rhs2   -- (X2)
    495 
    +      ...
    496 
    +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that
    497 
    +matches both equations yields the very same right hand side.  Example:
    498 
    +      And True True = True
    499 
    +      And a    True = a
    500 
    +The target (And True True) matches both equations but they then both
    501 
    +produce the same reduct True.
    502 
    +
    503 
    +More precisely (X1) and (X2) are /compatible/ iff
    504 
    +   If LHSs unify with a substitution S, then S(rhs1) = S(rhs2)
    505 
    +
    506 
    +Conversely, (X1) and (X2) are /incompatible/ if
    507 
    +   Their LHSs unify with S, and S(rhs1) /= S(rhs2)
    491 508
    492 
    -  1) The patterns are apart.
    509 
    +For open type families, only compatible instances are allowed. For closed
    510 
    +families, we use the Closed Family Matching Rule (see function `findBranch`):
    493 511
    494 
    -  2) The patterns unify with a substitution S, and their right hand sides
    495 
    -     are equal under that substitution.
    512 
    +    When looking up a target (F ty) in a closed type family F,
    513 
    +    find an equation (branch) such that:
    514 
    +      * the LHS matches the target
    515 
    +      * the target is apart from every previous /incompatible/ equation for F
    496 516
    497 
    -For open type families, only compatible instances are allowed. For closed
    498 
    -type families, the story is slightly more complicated. Consider the following:
    517 
    +We don't need to check the earlier equations that are compatible with the
    518 
    +matching equation, because they are either irrelevant (clause 1 of compatible)
    519 
    +or benign (clause 2 of compatible).
    520 
    +
    521 
    +Some examples:
    499 522
    500 
    -type family F a where
    501 
    -  F Int = Bool
    502 
    -  F a   = Int
    523 
    +  type family F a where
    524 
    +    F Int = Bool
    525 
    +    F a   = Int
    503 526
    504 
    -g :: Show a => a -> F a
    505 
    -g x = length (show x)
    527 
    +  g :: Show a => a -> F a
    528 
    +  g x = length (show x)
    506 529
    507 530 
     Should that type-check? No. We need to allow for the possibility that 'a'
    508 531 
     might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
    ... ... @@ -518,12 +541,12 @@ potentially-overlapping group is closed.
    518 541
    519 542 
     As another example, consider this:
    520 543
    521 
    -type family G x where
    522 
    -  G Int = Bool
    523 
    -  G a   = Double
    544 
    +  type family G x where
    545 
    +    G Int = Bool
    546 
    +    G a   = Double
    524 547
    525 
    -type family H y
    526 
    --- no instances
    548 
    +  type family H y
    549 
    +  -- no instances
    527 550
    528 551 
     Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
    529 552 
     simplify to be Int. So, (G (H Char)) is stuck, for now.
    ... ... @@ -531,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now.
    531 554 
     While everything above is quite sound, it isn't as expressive as we'd like.
    532 555 
     Consider this:
    533 556
    534 
    -type family J a where
    535 
    -  J Int = Int
    536 
    -  J a   = a
    557 
    +  type family J a where
    558 
    +    J Int = Int
    559 
    +    J a   = a
    537 560
    538 561 
     Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
    539 562 
     b is instantiated with Int, but the RHSs coincide there, so it's all OK.
    540 
    -
    541 
    -So, the rule is this: when looking up a branch in a closed type family, we
    542 
    -find a branch that matches the target, but then we make sure that the target
    543 
    -is apart from every previous *incompatible* branch. We don't check the
    544 
    -branches that are compatible with the matching branch, because they are either
    545 
    -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
    563 
    +Hence the Closed Family Matching Rule.
    546 564
    547 565 
     Note [Compatibility of eta-reduced axioms]
    548 566 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -574,15 +592,30 @@ fails anyway.
    574 592
    575 593 
     -- See Note [Compatibility]
    576 594 
     compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
    577 
    -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
    578 
    -                   (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
    595 
    +compatibleBranches b1 b2
    596 
    +  = case compareBranches b1 b2 of
    597 
    +       BC_Apart    -> True
    598 
    +       BC_Compat   -> True
    599 
    +       BC_Incompat -> False
    600 
    +
    601 
    +data BranchCompatibility
    602 
    +  = BC_Apart     -- LHSs are apart
    603 
    +  | BC_Compat    -- LHSs unify with S, and S(rhs1)=S(rhs2)
    604 
    +  | BC_Incompat  -- LHSs unify with S, and S(rhs1)/=S(rhs2)
    605 
    +
    606 
    +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility
    607 
    +compareBranches b1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
    608 
    +                b2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
    579 609 
       = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of
    580 610 
           -- Here we need the cab_tvs of the two branches to be disinct.
    581 611 
           -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom.
    582 
    -      SurelyApart     -> True
    583 
    -      MaybeApart {}   -> False
    584 
    -      Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
    612 
    +      SurelyApart     -> BC_Apart
    613 
    +      MaybeApart {}   -> pprPanic "compareBranches" (ppr b1 $$ ppr b2)
    614 
    +      Unifiable subst |  Type.substTyAddInScope subst rhs1 `eqType`
    585 615 
                              Type.substTyAddInScope subst rhs2
    616 
    +                      -> BC_Compat
    617 
    +                      | otherwise
    618 
    +                      -> BC_Incompat
    586 619 
       where
    587 620 
          (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
    588 621 
          -- See Note [Compatibility of eta-reduced axioms]
    ... ... @@ -630,10 +663,10 @@ injectiveBranches injectivity
    630 663 
               lhs1Subst = Type.substTys subst (getInjArgs lhs1)
    631 664 
               lhs2Subst = Type.substTys subst (getInjArgs lhs2)
    632 665
    633 
    --- takes a CoAxiom with unknown branch incompatibilities and computes
    634 
    --- the compatibilities
    635 
    --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
    636 666 
     computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
    667 
    +-- Takes a CoAxiom for a closed type family with place-holder
    668 
    +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields
    669 
    +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
    637 670 
     computeAxiomIncomps branches
    638 671 
       = snd (mapAccumL go [] branches)
    639 672 
       where
    ... ... @@ -641,11 +674,23 @@ computeAxiomIncomps branches
    641 674 
         go prev_brs cur_br
    642 675 
            = (new_br : prev_brs, new_br)
    643 676 
            where
    644 
    -         new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
    645 
    -
    646 
    -    mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
    647 
    -    mk_incomps prev_brs cur_br
    648 
    -       = filter (not . compatibleBranches cur_br) prev_brs
    677 
    +         (overlaps,incomps) = get_cab [] [] prev_brs
    678 
    +         new_br = cur_br { cab_overlaps = overlaps, cab_incomps  = incomps }
    679 
    +
    680 
    +         get_cab :: [CoAxBranch] -> [CoAxBranch]   -- Accumulators
    681 
    +                 -> [CoAxBranch]
    682 
    +                 -> ([CoAxBranch], [CoAxBranch])
    683 
    +         get_cab overlaps incomps [] = (overlaps,incomps)
    684 
    +         get_cab overlaps incomps (br:brs)
    685 
    +            = case compareBranches cur_br br of
    686 
    +                BC_Apart    -> get_cab overlaps      incomps      brs
    687 
    +                BC_Compat   -> get_cab (br:overlaps) incomps      brs
    688 
    +                BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs
    689 
    +
    690 
    +noAxiomIncomps :: CoAxBranch -> CoAxBranch
    691 
    +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps`
    692 
    +-- with [], because unbranched axioms have no "preceding" equations
    693 
    +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] }
    649 694
    650 695 
     {-
    651 696 
     ************************************************************************
    ... ... @@ -716,14 +761,15 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
    716 761 
                  -> SrcSpan
    717 762 
                  -> CoAxBranch
    718 763 
     mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
    719 
    -  = CoAxBranch { cab_tvs     = tvs'
    720 
    -               , cab_eta_tvs = eta_tvs'
    721 
    -               , cab_cvs     = cvs'
    722 
    -               , cab_lhs     = tidyTypes env lhs
    723 
    -               , cab_roles   = roles
    724 
    -               , cab_rhs     = tidyType env rhs
    725 
    -               , cab_loc     = loc
    726 
    -               , cab_incomps = placeHolderIncomps }
    764 
    +  = CoAxBranch { cab_tvs      = tvs'
    765 
    +               , cab_eta_tvs  = eta_tvs'
    766 
    +               , cab_cvs      = cvs'
    767 
    +               , cab_lhs      = tidyTypes env lhs
    768 
    +               , cab_roles    = roles
    769 
    +               , cab_rhs      = tidyType env rhs
    770 
    +               , cab_loc      = loc
    771 
    +               , cab_overlaps = placeHolderOverlaps
    772 
    +               , cab_incomps  = placeHolderIncomps }
    727 773 
       where
    728 774 
         (env1, tvs')     = tidyVarBndrs init_tidy_env tvs
    729 775 
         (env2, eta_tvs') = tidyVarBndrs env1          eta_tvs
    ... ... @@ -737,12 +783,12 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
    737 783
    738 784 
     -- all of the following code is here to avoid mutual dependencies with
    739 785 
     -- Coercion
    740 
    -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
    741 
    -mkBranchedCoAxiom ax_name fam_tc branches
    786 
    +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
    787 
    +mkBranchedCoAxiom role ax_name fam_tc branches
    742 788 
       = CoAxiom { co_ax_unique   = nameUnique ax_name
    743 789 
                 , co_ax_name     = ax_name
    744 790 
                 , co_ax_tc       = fam_tc
    745 
    -            , co_ax_role     = Nominal
    791 
    +            , co_ax_role     = role
    746 792 
                 , co_ax_implicit = False
    747 793 
                 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
    748 794
    ... ... @@ -753,7 +799,7 @@ mkUnbranchedCoAxiom ax_name fam_tc branch
    753 799 
                 , co_ax_tc       = fam_tc
    754 800 
                 , co_ax_role     = Nominal
    755 801 
                 , co_ax_implicit = False
    756 
    -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
    802 
    +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
    757 803
    758 804 
     mkSingleCoAxiom :: Role -> Name
    759 805 
                     -> [TyVar] -> [TyVar] -> [CoVar]
    ... ... @@ -768,7 +814,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
    768 814 
                 , co_ax_tc       = fam_tc
    769 815 
                 , co_ax_role     = role
    770 816 
                 , co_ax_implicit = False
    771 
    -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
    817 
    +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
    772 818 
       where
    773 819 
         branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
    774 820 
                               (map (const Nominal) tvs)
    ... ... @@ -786,7 +832,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
    786 832 
                 , co_ax_implicit = True  -- See Note [Implicit axioms] in GHC.Core.TyCon
    787 833 
                 , co_ax_role     = Representational
    788 834 
                 , co_ax_tc       = tycon
    789 
    -            , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
    835 
    +            , co_ax_branches = unbranched (noAxiomIncomps branch) }
    790 836 
       where
    791 837 
         branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
    792 838 
                               roles (getSrcSpan name)
    ... ... @@ -1224,7 +1270,9 @@ findBranch :: Array BranchIndex CoAxBranch
    1224 1270 
                -> Maybe (BranchIndex, [Type], [Coercion])
    1225 1271 
         -- coercions relate requested types to returned axiom LHS at role N
    1226 1272 
     findBranch branches target_tys
    1227 
    -  = foldr go Nothing (assocs branches)
    1273 
    +  = -- Implements the Closed Family Matching Rule
    1274 
    +    -- in Note [Compatibility]
    1275 
    +    foldr go Nothing (assocs branches)
    1228 1276 
       where
    1229 1277 
         go :: (BranchIndex, CoAxBranch)
    1230 1278 
            -> Maybe (BranchIndex, [Type], [Coercion])
    ... ... @@ -1264,8 +1312,8 @@ noEarlierMatchCheck
    1264 1312 
       :: [Type]
    1265 1313 
       -> CoAxBranch -- ^ The candidate equation we wish to use
    1266 1314 
       -> Bool       -- ^ True <=> equation can fire
    1267 
    -noEarlierMatchCheck target (CoAxBranch { cab_incomps = incomps })
    1268 
    -  = not (any matches incomps)
    1315 
    +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps })
    1316 
    +  = not (any matches overlaps)
    1269 1317 
       where
    1270 1318 
         matches earlier_branch
    1271 1319 
           = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target)

  • compiler/GHC/IfaceToCore.hs
    ... ... @@ -903,12 +903,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
    903 903 
            -- See #13803
    904 904 
            ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
    905 905 
                           $ tc_ax_branches branches
    906 
    -       ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
    907 
    -                             , co_ax_name     = tc_name
    908 
    -                             , co_ax_tc       = tc_tycon
    909 
    -                             , co_ax_role     = role
    910 
    -                             , co_ax_branches = manyBranches tc_branches
    911 
    -                             , co_ax_implicit = False }
    906 
    +       ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches
    912 907 
            ; return (ACoAxiom axiom) }
    913 908
    914 909 
     tc_iface_decl _ _ (IfacePatSyn{ ifName = name
    ... ... @@ -1124,7 +1119,7 @@ tc_ax_branch prev_branches
    1124 1119 
                                 , ifaxbEtaTyVars = eta_tv_bndrs
    1125 1120 
                                 , ifaxbCoVars = cv_bndrs
    1126 1121 
                                 , ifaxbLHS = lhs, ifaxbRHS = rhs
    1127 
    -                            , ifaxbRoles = roles, ifaxbIncomps = incomps })
    1122 
    +                            , ifaxbRoles = roles, ifaxbIncomps = _incomps })
    1128 1123 
       = bindIfaceTyConBinders_AT
    1129 1124 
           (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
    1130 1125 
              -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
    ... ... @@ -1135,14 +1130,15 @@ tc_ax_branch prev_branches
    1135 1130 
         ; this_mod <- getIfModule
    1136 1131 
         ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS`
    1137 1132 
                                       moduleNameFS (moduleName this_mod))
    1138 
    -          br = CoAxBranch { cab_loc     = loc
    1139 
    -                          , cab_tvs     = binderVars tvs
    1140 
    -                          , cab_eta_tvs = eta_tvs
    1141 
    -                          , cab_cvs     = cvs
    1142 
    -                          , cab_lhs     = tc_lhs
    1143 
    -                          , cab_roles   = roles
    1144 
    -                          , cab_rhs     = tc_rhs
    1145 
    -                          , cab_incomps = map (prev_branches `getNth`) incomps }
    1133 
    +          br = CoAxBranch { cab_loc      = loc
    1134 
    +                          , cab_tvs      = binderVars tvs
    1135 
    +                          , cab_eta_tvs  = eta_tvs
    1136 
    +                          , cab_cvs      = cvs
    1137 
    +                          , cab_lhs      = tc_lhs
    1138 
    +                          , cab_roles    = roles
    1139 
    +                          , cab_rhs      = tc_rhs
    1140 
    +                          , cab_overlaps = placeHolderOverlaps
    1141 
    +                          , cab_incomps  = placeHolderIncomps }
    1146 1142 
         ; return (prev_branches ++ [br]) }
    1147 1143
    1148 1144 
     tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -1047,7 +1047,7 @@ Note [Exploiting closed type families].
    1047 1047 
         You might think that (B3) could be instantiated to Bak Char ~ Char; but
    1048 1048 
         actually that instantiation will never fire because (B2) Bak Char ~ Int would
    1049 1049 
         fire first.  So the only way to return a Char is via (B1); so we
    1050 
    -    can emit [W] alpha ~ Int.  Hence (B3) is not relevant; only (B2) is relevant.
    1050 
    +    can emit [W] alpha ~ Int.  Hence (B3) is not relevant; only (B1) is relevant.
    1051 1051
    1052 1052 
         That is the reason for condition (R2) in the definition of Relevance above.
    1053 1053 
         A watertight proof that this is the Right Thing is not very easy.  See more
    ... ... @@ -1072,6 +1072,23 @@ Note [Exploiting closed type families].
    1072 1072 
              TMessage @SC @Req alpha
    1073 1073 
         and equation (T1) does not match that. (It does unify, but we don't care.)
    1074 1074
    1075 
    +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/
    1076 
    +    earlier equation matches, not just no earlier /incompatible/ equation
    1077 
    +    matches.  Consider T27282a:
    1078 
    +        type family F a where
    1079 
    +          F Int  = Int  -- B1
    1080 
    +          F Char = Bool -- B2
    1081 
    +          F a    = a    -- B3
    1082 
    +
    1083 
    +        [W] F alpha ~ Int
    1084 
    +
    1085 
    +    (B1) is relevant, and (B2) is not. What about (B3)?  It pre-unifies with
    1086 
    +    the Wanted via [alpha :-> Int, a :-> Int].  But under that substitution
    1087 
    +    (B1) would fire, so (B3) is not relevant.
    1088 
    +
    1089 
    +    And yet, (B1) is /compatible/ with (B3), so it's no good just looking at
    1090 
    +    the `cab_incomps` of (B3).  Instead we look at `cab_overlaps`.
    1091 
    +
    1075 1092 
     Note [Exploiting open type families] see `mkTopOpenFamEqFDs`
    1076 1093 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1077 1094 
     Generating fundeps from a top-level type instance is covered in Section 5.2 in
    ... ... @@ -1451,6 +1468,8 @@ solveFunDeps work_ev fd_eqns
    1451 1468 
                              ; uPairsTcM uenv eqs }
    1452 1469
    1453 1470 
     instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn]
    1471 
    +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
    1472 
    +--     Wrinkle (IMP1)
    1454 1473 
     instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
    1455 1474 
       | null qtvs
    1456 1475 
       = return rev_eqs
    ... ... @@ -1463,11 +1482,9 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
    1463 1482 
            -- (reverse eqs): See Note [Reverse order of fundep equations]
    1464 1483
    1465 1484 
         subst_pair subst (Pair ty1 ty2)
    1466 
    -       = Pair (substTy subst' ty1) (substTy subst' ty2)
    1467 
    --- ToDo not correct!
    1485 
    +       = Pair (substTy subst' ty1) ty2
    1468 1486 
                   -- ty2 does not mention fd_qtvs, so no need to subst it.
    1469 
    -              -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
    1470 
    -              --     Wrinkle (IMP1)
    1487 
    +              -- See invariant on `fv_eqs` in `data FunDepEqns`.
    1471 1488 
            where
    1472 1489 
              subst' = extendSubstInScopeSet subst (tyCoVarsOfTypes [ty1,ty2])
    1473 1490 
                       -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result

  • compiler/GHC/Tc/TyCl.hs
    ... ... @@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
    3462 3462
    3463 3463 
            ; let mb_co_ax
    3464 3464 
                   | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
    3465 
    -              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
    3465 
    +              | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches)
    3466 3466
    3467 3467 
                  fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig)
    3468 3468 
                           (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj'

  • testsuite/tests/indexed-types/should_compile/all.T
    ... ... @@ -317,3 +317,4 @@ test('T25611c', normal, compile, [''])
    317 317 
     test('T25611d', normal, compile, [''])
    318 318 
     test('T25657', normal, compile, [''])
    319 319 
     test('T27828', normal, compile, [''])
    320 
    +test('T27828a', normal, compile, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help Notification message regarding https://gitlab.haskell.org/ghc/ghc/-/commit/b9431ef21af13163fdfde045cd1f5008c6a3b459 at 1790260985