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

Commits:

3 changed files:

Changes:

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -25,7 +25,7 @@ import GHC.Core.FamInstEnv
    25 25
     import GHC.Core.Coercion
    
    26 26
     import GHC.Core.Predicate( EqRel(..) )
    
    27 27
     import GHC.Core.TyCon
    
    28
    -import GHC.Core.Unify( tcUnifyTyForInjectivity, typeListsAreApart, typesAreApart, tcUnifyTy )
    
    28
    +import GHC.Core.Unify( tcUnifyTyForInjectivity, typeListsAreApart, typesAreApart )
    
    29 29
     import GHC.Core.Coercion.Axiom
    
    30 30
     import GHC.Core.TyCo.Subst( elemSubst )
    
    31 31
     
    
    ... ... @@ -38,7 +38,7 @@ import GHC.Utils.Outputable
    38 38
     import GHC.Utils.Panic
    
    39 39
     
    
    40 40
     import GHC.Data.Pair
    
    41
    -import Data.Maybe( mapMaybe, isJust )
    
    41
    +import Data.Maybe( mapMaybe )
    
    42 42
     
    
    43 43
     
    
    44 44
     {- Note [Overview of functional dependencies in type inference]
    
    ... ... @@ -500,7 +500,8 @@ tryFamEqFunDeps fam_tc args work_item@(EqCt { eq_ev = ev, eq_rhs = rhs })
    500 500
       | Just ax <- isClosedFamilyTyCon_maybe fam_tc
    
    501 501
       = -- Closed type families
    
    502 502
         do { -- Note [Do local fundeps before top-level instances]
    
    503
    -         case tyConInjectivityInfo fam_tc of
    
    503
    +         simpleStage $ traceTcS "fundep closed" (ppr fam_tc)
    
    504
    +       ; case tyConInjectivityInfo fam_tc of
    
    504 505
                NotInjective  -> nopStage()
    
    505 506
                Injective inj -> tryFDEqns fam_tc args work_item $
    
    506 507
                                 mkLocalUserFamEqFDs fam_tc inj args rhs
    
    ... ... @@ -531,7 +532,9 @@ tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eq
    531 532
     -----------------------------------------
    
    532 533
     mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns]
    
    533 534
     mkTopClosedFamEqFDs ax work_args work_rhs
    
    534
    -  = return (go (fromBranches (coAxiomBranches ax)))
    
    535
    +  = do { let branches = fromBranches (coAxiomBranches ax)
    
    536
    +       ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)
    
    537
    +       ; return (go branches) }
    
    535 538
       where
    
    536 539
         go :: [CoAxBranch] -> [FunDepEqns]
    
    537 540
         go [] = []
    
    ... ... @@ -539,18 +542,19 @@ mkTopClosedFamEqFDs ax work_args work_rhs
    539 542
         go (branch : later_branches)
    
    540 543
           | CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys
    
    541 544
                        , cab_rhs = rhs_ty, cab_incomps = incomps } <- branch
    
    542
    -      , not (work_args `typeListsAreApart` lhs_tys)
    
    543
    -      , isJust (tcUnifyTy work_rhs rhs_ty)
    
    544
    -      = if all ok incomps && all ok later_branches
    
    545
    +      , not (no_match lhs_tys rhs_ty)
    
    546
    +      = if all no_match_branch incomps && all no_match_branch later_branches
    
    545 547
             then [FDEqns { fd_qtvs = qtvs, fd_eqs = zipWith Pair lhs_tys work_args }]
    
    546 548
             else []
    
    547 549
     
    
    548 550
           | otherwise
    
    549 551
           = go later_branches
    
    550 552
     
    
    551
    -    ok (CoAxBranch { cab_lhs = lhs_tys, cab_rhs = rhs_ty })
    
    552
    -      = work_args `typeListsAreApart` lhs_tys ||
    
    553
    -        work_rhs  `typesAreApart`     rhs_ty
    
    553
    +    no_match_branch (CoAxBranch { cab_lhs = lhs_tys, cab_rhs = rhs_ty })
    
    554
    +      = no_match lhs_tys rhs_ty
    
    555
    +
    
    556
    +    no_match lhs_tys rhs_ty = work_args `typeListsAreApart` lhs_tys ||
    
    557
    +                              work_rhs  `typesAreApart`     rhs_ty
    
    554 558
     
    
    555 559
     mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> Xi -> TcS [FunDepEqns]
    
    556 560
     -- Implements (INJFAM:Wanted/top)
    

  • testsuite/tests/indexed-types/should_compile/CEqCanOccursCheck.hs
    ... ... @@ -8,10 +8,13 @@ type family F a where
    8 8
     type family G a b where
    
    9 9
       G a a = a
    
    10 10
     
    
    11
    -{-
    
    11
    +{- Ambiguity check for foo
    
    12
    +[G] F a ~ a
    
    13
    +[G] F a ~ b
    
    14
    +
    
    12 15
     [W] F alpha ~ alpha
    
    13 16
     [W] F alpha ~ beta
    
    14
    -[W] G alpha beta ~ Int
    
    17
    +[W] G alpha beta ~ G a b
    
    15 18
     -}
    
    16 19
     
    
    17 20
     foo :: (F a ~ a, F a ~ b) => G a b -> ()
    

  • testsuite/tests/indexed-types/should_fail/T12522a.hs
    ... ... @@ -21,3 +21,9 @@ def = undefined
    21 21
     
    
    22 22
     -- test :: Uncurried [Int, String] String
    
    23 23
     test = def $ \n s -> I $ show n ++ s
    
    24
    +
    
    25
    +{-
    
    26
    +Arg to `def` has type (alpha -> String -> String)
    
    27
    +So we get
    
    28
    +  [W] Curry as0 b0 ~ (alpha -> String -> String)
    
    29
    +-}