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

Commits:

13 changed files:

Changes:

  • changelog.d/T27844
    1 
    +section: compiler
    2 
    +issues: #27844
    3 
    +mrs: !16723
    4 
    +synopsis:
    5 
    +  Reinstate a missing occurs check in the constraint solver
    6 
    +description:
    7 
    +  Simplifies code in GHC's type-constraint solver, thereby fixing an outright
    8 
    +  compiler loop (via a missing occurs check).
    9 
    +

  • compiler/GHC/Runtime/Heap/Inspect.hs
    ... ... @@ -630,7 +630,7 @@ be sigmas and not taus.
    630 630 
     ~~~~~~~~~~~~~~~~~~~~~~
    631 631 
     In the GHCi debugger we use unification variables whose MetaInfo is
    632 632 
     RuntimeUnkTv.  The special property of a RuntimeUnkTv is that it can
    633 
    -unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq).
    633 
    +unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification).
    634 634 
     If we don't do this `:print <term>` will fail if the type of <term>
    635 635 
     has nested `forall`s or `=>`s.
    636 636

  • compiler/GHC/Tc/Errors.hs
    ... ... @@ -581,7 +581,6 @@ mkErrorItem ct
    581 581 
                                CtGiven {}                               -> Nothing
    582 582 
                                CtWanted (WantedCt { ctev_dest = dest }) -> Just dest
    583 583
    584 
    -
    585 584 
                  m_reason = case ct of
    586 585 
                     CIrredCan (IrredCt { ir_reason = reason }) -> Just reason
    587 586 
                     _                                          -> Nothing

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence
    21 21 
     import GHC.Tc.Types.Constraint
    22 22 
     import GHC.Tc.Types.CtLoc
    23 23 
     import GHC.Tc.Types.Origin
    24 
    +import GHC.Tc.Types( TcM )
    24 25 
     import GHC.Tc.Utils.Unify
    25 26 
     import GHC.Tc.Utils.TcType
    26 27 
     import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe )
    ... ... @@ -36,8 +37,8 @@ import GHC.Core.Coercion
    36 37 
     import GHC.Core.Reduction
    37 38 
     import GHC.Core.FamInstEnv ( FamInstEnvs )
    38 39 
     import GHC.Core
    39 
    -import GHC.Types.Var
    40 40
    41 
    +import GHC.Types.Var
    41 42 
     import GHC.Types.Basic
    42 43 
     import GHC.Types.Name.Reader
    43 44 
     import GHC.Types.Var.Env
    ... ... @@ -49,6 +50,8 @@ import GHC.Utils.Misc
    49 50 
     import GHC.Utils.Monad
    50 51
    51 52 
     import GHC.Data.Pair
    53 
    +import GHC.Data.Bag
    54 
    +
    52 55 
     import Control.Monad
    53 56 
     import Data.Maybe ( isJust, isNothing )
    54 57 
     import Data.List  ( zip4 )
    ... ... @@ -406,11 +409,13 @@ canonicaliseEquality
    406 409 
     --   hold.
    407 410
    408 411 
     canonicaliseEquality ev eq_rel ty1 ty2
    409 
    -  = Stage $ do { traceTcS "canonicaliseEquality" $
    412 
    +  = Stage $ do { traceTcS "canonicaliseEquality {" $
    410 413 
                      vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ]
    411 414 
                    ; rdr_env   <- getGlobalRdrEnvTcS
    412 415 
                    ; fam_insts <- getFamInstEnvs
    413 
    -               ; can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
    416 
    +               ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2
    417 
    +               ; traceTcS "canonicaliseEquality }" (ppr res)
    418 
    +               ; return res }
    414 419
    415 420 
     -- | Main worker function for 'canonicaliseEquality'.
    416 421 
     --
    ... ... @@ -1822,7 +1827,7 @@ Ticket #10009, a very nasty example:
    1822 1827 
         g :: forall a. (UnF (F a) ~ a) => a -> ()
    1823 1828 
         g _ = f (undefined :: F a)
    1824 1829
    1825 
    -For g we get [G]  g1 : UnF (F a) ~ a
    1830 
    +For g we get [G] g1 : UnF (F a) ~ a
    1826 1831 
                  [W] w1 : UnF (F beta) ~ beta
    1827 1832 
                  [W] w2 : F a ~ F beta
    1828 1833
    ... ... @@ -1982,7 +1987,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
    1982 1987 
         finish rewriters kind_co
    1983 1988 
           = do { traceTcS "Hetero equality gives rise to kind equality"
    1984 1989 
                      (ppr swapped $$
    1985 
    -                  ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
    1990 
    +                  ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
    1986 1991 
                ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn rewriters
    1987 1992 
                     -- rewriteEqEvidence adds any as-yet-unsolved equalities
    1988 1993 
                     -- from the kind equality (namely `rewriters`) to the
    ... ... @@ -2040,15 +2045,15 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
    2040 2045 
              then finish_with_swapping
    2041 2046 
              else finish_without_swapping }
    2042 2047
    2043 
    -  | TyVarLHS {} <- lhs1
    2048 
    +  | TyVarLHS tv <- lhs1
    2044 2049 
       , TyFamLHS {} <- lhs2
    2045 
    -  = if put_tyvar_on_lhs
    2050 
    +  = if mightPossiblyUnify ev eq_rel tv
    2046 2051 
         then finish_without_swapping
    2047 2052 
         else finish_with_swapping
    2048 2053
    2049 2054 
       | TyFamLHS {} <- lhs1
    2050 
    -  , TyVarLHS {} <- lhs2
    2051 
    -  = if put_tyvar_on_lhs
    2055 
    +  , TyVarLHS tv <- lhs2
    2056 
    +  = if mightPossiblyUnify ev eq_rel tv
    2052 2057 
         then finish_with_swapping
    2053 2058 
         else finish_without_swapping
    2054 2059
    ... ... @@ -2096,10 +2101,6 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
    2096 2101 
                ; new_ev <-rewriteEqEvidence ev swapped lhs1_redn lhs2_redn emptyCoHoleSet
    2097 2102 
                ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
    2098 2103
    2099 
    -    put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
    2100 
    -    -- See Note [Orienting TyVarLHS/TyFamLHS]
    2101 
    -    -- Same conditions as for canEqCanLHSFinish_try_unification
    2102 
    -    -- which we are setting ourselves up for here
    2103 2104
    2104 2105 
     {- Note [Orienting TyVarLHS/TyFamLHS]
    2105 2106 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -2108,16 +2109,16 @@ Which to put on the left? Answer:
    2108 2109
    2109 2110 
     * If there is no chance of unifying, put the type family on the left,
    2110 2111 
       (F tys ~ a), because it's generally better to rewrite away function
    2111 
    -  calls.  See `put_tyvar_on_lhs` in canEqCanLHS2; and
    2112 
    -  Note [Orienting TyVarLHS/TyFamLHS]
    2112 
    +  calls.  For the "no chance of unifying" test, see calls to
    2113 
    +  `mightPossiblyUnify` in `canEqCanLHS2; and Note [Orienting TyVarLHS/TyFamLHS]
    2113 2114
    2114 2115 
     * But if there /is/ a chance of unifying, put the tyvar on the left,
    2115 2116 
       (a ~ F tys), as this may be our only shot to unify. Again see
    2116 
    -  `put_tyvar_on_lhs`.
    2117 
    +  `mightPossiblyUnify`.
    2117 2118
    2118 2119 
     * But if we /fail/ to unify then flip back to (F tys ~ a) because it's
    2119 
    -  generally better to rewrite away function calls. See the call to
    2120 
    -  `swapAndFinish` in `canEqCanLHSFinish_try_unification`
    2120 
    +  generally better to rewrite away function calls. See the swapping-back
    2121 
    +  code in `finish_on_unify` in `canEqCanLHSFinish_try_unification`
    2121 2122
    2122 2123 
       It's important to flip back. Consider
    2123 2124 
         [W] F alpha ~ alpha
    ... ... @@ -2197,71 +2198,64 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
    2197 2198 
           = return True
    2198 2199
    2199 2200 
     -----------------------
    2200 
    -canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    2201 
    -  -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
    2202 
    -  | CtWanted wev <- ev         -- See Note [Do not unify Givens]
    2201 
    +mightPossiblyUnify :: CtEvidence -> EqRel -> TcTyVar -> Bool
    2202 
    +-- Is this equality (tv ~ ty) one we could perhaps solve by unification?
    2203 
    +--    True  <=> perhaps yes
    2204 
    +--    False <=> definitely not
    2205 
    +mightPossiblyUnify ev eq_rel tv
    2206 
    +  | isMetaTyVar tv
    2207 
    +  , CtWanted wev <- ev         -- See Note [Do not unify Givens]
    2203 2208 
       , NomEq <- eq_rel            -- See Note [Do not unify representational equalities]
    2204 2209 
       , wantedCtHasNoRewriters wev -- See Note [Unify only if the rewriter set is empty]
    2205 
    -  , TyVarLHS lhs_tv <- lhs
    2210 
    +  = True
    2211 
    +  | otherwise
    2212 
    +  = False
    2213 
    +
    2214 
    +canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    2215 
    +  -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
    2216 
    +  | TyVarLHS lhs_tv <- lhs
    2217 
    +  , mightPossiblyUnify ev eq_rel lhs_tv
    2206 2218 
       = do  { given_eq_lvl <- getInnermostGivenEqLevel
    2207 2219 
             ; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of
    2208 
    -            SUC_CanUnify ->
    2209 
    -              unify lhs_tv (mkReflRedn Nominal rhs)
    2210 
    -            SUC_CannotUnify
    2211 
    -              | Just can_rhs <- canTyFamEqLHS_maybe rhs
    2212 
    -              -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
    2213 
    -              | otherwise
    2214 
    -              -> finish_no_unify
    2215 
    -            SUC_NotSure ->
    2216 
    -              -- We have a touchable unification variable on the left,
    2220 
    +            SUC_CannotUnify -> finish_no_unify
    2221 
    +            SUC_CanUnify    -> do_unification lhs_tv (mkReflRedn Nominal rhs)
    2222 
    +            SUC_NotSure     ->
    2223 
    +              -- We have a touchable, unfilled unification variable on the left,
    2217 2224 
                   -- and the top-shape check succeeded. These are both guaranteed
    2218 2225 
                   -- by the fact that simpleUnifyCheck did not return SUC_CannotUnify.
    2226 
    +              --
    2227 
    +              -- Next, do a full `checkTyEqRhs` check to see if we can unify
    2228 
    +              -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify
    2219 2229 
                   do  { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv
    2220 2230 
                       ; check_result <- wrapTcS (checkTyEqRhs flags rhs)
    2231 
    +                  ; traceTcS "canEqCanLHSFinish_try_unification" $
    2232 
    +                    vcat [ text "lhs" <+> ppr lhs
    2233 
    +                         , text "rhs" <+> ppr rhs
    2234 
    +                         , text "check_result" <+> ppr check_result ]
    2221 2235 
                       ; case check_result of
    2222 
    -                      PuOK cts rhs_redn ->
    2223 
    -                        do { emitWork cts
    2224 
    -                           ; unify lhs_tv rhs_redn }
    2225 
    -                      PuFail reason
    2226 
    -                        | Just can_rhs <- canTyFamEqLHS_maybe rhs
    2227 
    -                        -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
    2228 
    -                        | reason `cterHasOnlyProblems` do_not_prevent_rewriting
    2229 
    -                        ->
    2230 
    -                          -- ContinueWith, to allow using this constraint for
    2231 
    -                          -- rewriting (e.g. alpha[2] ~ beta[3]).
    2232 
    -                          do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
    2233 
    -                             ; continueWith $ Right $
    2234 
    -                                 EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
    2235 
    -                                      , eq_lhs = lhs , eq_rhs = rhs }
    2236 
    -                             }
    2237 
    -                        | otherwise
    2238 
    -                        -> try_irred reason
    2239 
    -                  }
    2236 
    +                      PuFail {}         -> finish_no_unify
    2237 
    +                      PuOK cts rhs_redn -> do { emitWork cts
    2238 
    +                                              ; do_unification lhs_tv rhs_redn } }
    2240 2239 
              }
    2241 2240 
       -- Otherwise unification is off the table
    2242 2241 
       | otherwise
    2243 2242 
       = finish_no_unify
    2244 2243
    2245 2244 
       where
    2246 
    -    -- We can't unify, but this equality can go in the inert set
    2247 
    -    -- and be used to rewrite other constraints.
    2248 
    -    finish_no_unify =
    2249 
    -      canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    2250 
    -
    2251 
    -    -- We can't unify, and this equality should not be used to rewrite
    2252 
    -    -- other constraints (e.g. because it has an occurs check).
    2253 
    -    -- So add it to the inert Irreds.
    2254 
    -    try_irred reason =
    2255 
    -      tryIrredInstead reason ev eq_rel swapped lhs rhs
    2256 
    -
    2257 
    -    -- We can't unify as-is, and want to flip the equality around.
    2258 
    -    -- Example: alpha ~ F tys, flip it around to become the canonical
    2259 
    -    -- equality f tys ~ alpha.
    2260 
    -    swap_and_finish tv can_rhs =
    2261 
    -      swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
    2262 
    -
    2263 
    -    -- Phew! Finally!  We can unify; go ahead and do so.
    2264 
    -    unify tv rhs_redn =
    2245 
    +    -- finish_no_unify: abandon the attempt to unify, and instead hand off to
    2246 
    +    -- canEqCanLHSFinish_no_unification
    2247 
    +    -- First, though, if we have (tv ~ F tys)
    2248 
    +    --        swap it over so we get (F tys ~ tv), with `F tys` on the LHS
    2249 
    +    -- See Note [Orienting TyVarLHS/TyFamLHS]
    2250 
    +    finish_no_unify
    2251 
    +      | TyVarLHS lhs_tv <- lhs
    2252 
    +      , Just can_rhs <- canTyFamEqLHS_maybe rhs
    2253 
    +      = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv)
    2254 
    +      | otherwise
    2255 
    +      = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    2256 
    +
    2257 
    +    -- do_unification: Phew! Finally!  We can unify; go ahead and do so.
    2258 
    +    do_unification tv rhs_redn =
    2265 2259 
           do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
    2266 2260 
                -- the evidence, even if swapped=IsSwapped.   Suppose the original was
    2267 2261 
                --     [W] co : Int ~ alpha
    ... ... @@ -2273,7 +2267,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    2273 2267 
                          else rewriteEqEvidence ev swapped
    2274 2268 
                                   (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
    2275 2269 
                                   emptyCoHoleSet
    2276 
    -                              -- emptyCoHoleSet: rhs_redn has no CoercionHoles
    2270 
    +                              -- emptyCoHoleSet: we are about to /solve/ this
    2271 
    +                              -- constraint, so its CoHoleSet doesn't matter
    2277 2272
    2278 2273 
              ; let tv_ty     = mkTyVarTy tv
    2279 2274 
                    final_rhs = reductionReducedType rhs_redn
    ... ... @@ -2297,45 +2292,48 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    2297 2292 
              ; return (Stop new_ev (text "Solved by unification")) }
    2298 2293
    2299 2294 
     ---------------------------
    2300 
    --- Unification is off the table
    2301 2295 
     canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    2302 
    -  = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
    2296 
    +  -- We can't unify, but we can see if this equality can go in the inert set
    2297 
    +  -- and be used to rewrite other constraints.
    2298 
    +  -- See Note [Equalities where unification fails]
    2299 
    +  = do { -- Do checkTypeEqNoUnification to guarantee (TyEq:OC), (TyEq:F)
    2303 2300 
              -- Must do the occurs check even on tyvar/tyvar equalities,
    2304 2301 
              -- in case have  x ~ (y :: ..x...); this is #12593.
    2305 
    -       ; check_result <- checkTypeEq ev eq_rel lhs rhs
    2306 
    -
    2307 
    -       ; let lhs_ty = canEqLHSType lhs
    2302 
    +       ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs
    2308 2303 
            ; case check_result of
    2309 2304 
                 PuFail reason
    2310 
    -
    2311 
    -              -- If we had F a ~ G (F a), which gives an occurs check,
    2312 
    -              -- then swap it to G (F a) ~ F a, which does not
    2313 
    -              -- However `swap_for_size` above will orient it with (G (F a)) on
    2314 
    -              -- the left anwyway.  `swap_for_rewriting` "wins", but that doesn't
    2315 
    -              -- matter: in the occurs check case swap_for_rewriting will be moot.
    2316 
    -              -- TL;DR: the next four lines of code are redundant
    2317 
    -              -- I'm leaving them here in case they become relevant again
    2318 
    ---              | TyFamLHS {} <- lhs
    2319 
    ---              , Just can_rhs <- canTyFamEqLHS_maybe rhs
    2320 
    ---              , reason `cterHasOnlyProblem` cteSolubleOccurs
    2321 
    ---              -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs
    2322 
    ---              | otherwise
    2323 
    -
    2324 
    -              | reason `cterHasOnlyProblems` do_not_prevent_rewriting
    2325 
    -              -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
    2326 
    -                    ; continueWith $ Right $
    2327 
    -                        EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
    2328 
    -                             , eq_lhs = lhs , eq_rhs = rhs }
    2329 
    -                    }
    2330 
    -
    2331 
    -              | otherwise
    2332 
    -              -> tryIrredInstead reason ev eq_rel swapped lhs rhs
    2305 
    +              -> -- We can't unify, and this equality should not be used to rewrite
    2306 
    +                 -- other constraints (e.g. because it has an occurs check).
    2307 
    +                 -- So add it to the inert Irreds.
    2308 
    +                 -- NB: The `reason` will never include `cteConcrete` or `cteSkolemEscape`
    2309 
    +                 --     because checkTypeEqNoUnification doesn't check for those things;
    2310 
    +                 --     they do not prevent the equality being canonical.  So you can't
    2311 
    +                 --     rely on `reason` reporting those points, nor do we need to.
    2312 
    +                 do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
    2313 
    +                    ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
    2333 2314
    2334 2315 
                 PuOK new_eqs rhs_redn
    2335 
    -              -> do { emitWork new_eqs
    2336 
    -                    ; let new_holes = rewriterSetFromCts new_eqs
    2316 
    +              -> -- Put this constraint into the inert set, so that it will be used
    2317 
    +                 -- to solve or rewrite other constraints.
    2318 
    +                 --
    2319 
    +                 -- NB: checkTypeEqNoUnification does not check for
    2320 
    +                 --     (a) skolem-escape (tefTyVar_levelCheck = LC_None)
    2321 
    +                 --     (b) concreteness  (tefTyVar_concreteCheck = CC_None)
    2322 
    +                 --   So an equality whose only problem is e.g. skolem-escape will
    2323 
    +                 --   return PuOK, will be put in the inert set, will be used for
    2324 
    +                 --   rewriting. That is fine.
    2325 
    +                 --
    2326 
    +                 -- assertPpr (isEmptyCts new_eqs):
    2327 
    +                 --   checkTypeEqNoUnification does neither promotion nor type-family
    2328 
    +                 --   flattening for Wanteds, and hence creates no equalities to solve
    2329 
    +                 assertPpr (isEmptyCts new_eqs)
    2330 
    +                    (vcat [ text "new_eqs"  <+> ppr new_eqs
    2331 
    +                          , text "rhs_redn" <+> ppr rhs_redn
    2332 
    +                          , text "lhs"      <+> ppr lhs
    2333 
    +                          , text "rhs"      <+> ppr rhs ]) $
    2334 
    +                 do { let lhs_ty    = canEqLHSType lhs
    2337 2335 
                               lhs_redn  = mkReflRedn (eqRelRole eq_rel) lhs_ty
    2338 
    -                    ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes
    2336 
    +                    ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet
    2339 2337
    2340 2338 
                         -- Important: even if the coercion is Refl,
    2341 2339 
                         --   * new_ev has reductionReducedType on the RHS
    ... ... @@ -2346,45 +2344,56 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    2346 2344 
                                , eq_lhs = lhs
    2347 2345 
                                , eq_rhs = reductionReducedType rhs_redn } } }
    2348 2346
    2349 
    --- | Some problems prevent /unification/ but not /rewriting/:
    2350 
    ---
    2351 
    --- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
    2352 
    ---    we can't unify (skolem-escape); but it /is/ canonical,
    2353 
    ---    and hence we /can/ use it for rewriting
    2354 
    ---
    2355 
    --- Concrete-ness:  alpha[conc] ~ b[sk]
    2356 
    ---    We can use it to rewrite; we still have to solve the original
    2357 
    -do_not_prevent_rewriting :: CheckTyEqResult
    2358 
    -do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
    2359 
    -                           cteProblem cteConcrete
    2347 
    +checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType
    2348 
    +                         -> TcS (PuResult Ct Reduction)
    2349 
    +-- Used for general CanEqLHSs, when we have decided that we cannot unify
    2350 
    +checkTypeEqNoUnification ev eq_rel lhs rhs =
    2351 
    +  case ev of
    2352 
    +    CtGiven {} ->
    2353 
    +      do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs
    2354 
    +                                                  , text "rhs:" <+> ppr rhs ])
    2355 
    +         ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
    2356 
    +         ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
    2357 
    +         ; case check_result of
    2358 
    +              PuFail reason -> return (PuFail reason)
    2359 
    +              PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
    2360 
    +                                  ; emitWork new_givens
    2361 
    +                                  ; updInertSet (addCycleBreakerBindings prs)
    2362 
    +                                  ; return (pure redn) } }
    2363 
    +    CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $
    2364 
    +                        vcat [ text "lhs:" <+> ppr lhs
    2365 
    +                             , text "rhs:" <+> ppr rhs ]
    2366 
    +                      ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
    2367 
    +                      ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
    2368 
    +                      ; return check_result }
    2369 
    +  where
    2370 
    +    wanted_flags :: TyEqFlags TcM Ct
    2371 
    +    wanted_flags = notUnifying_TEFTask occ_prob lhs
    2372 
    +        -- See Note [Don't cycle-break Wanteds when not unifying]
    2373 
    +
    2374 
    +    given_flags :: TyEqFlags TcM (TcTyVar, TcType)
    2375 
    +    given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
    2376 
    +        -- TEFA_Break used for: [G] a ~ Maybe (F a)
    2377 
    +        --                   or [G] F a ~ Maybe (F a)
    2378 
    +
    2379 
    +    -- occ_prob: see Note [Occurs check and representational equality]
    2380 
    +    occ_prob = case eq_rel of
    2381 
    +                 NomEq  -> cteInsolubleOccurs
    2382 
    +                 ReprEq -> cteSolubleOccurs
    2383 
    +
    2384 
    +    ---------------------------
    2385 
    +    mk_new_given :: (TcTyVar, TcType) -> TcS Ct
    2386 
    +    mk_new_given (new_tv, fam_app)
    2387 
    +      = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
    2388 
    +      where
    2389 
    +        new_ty     = mkTyVarTy new_tv
    2390 
    +        given_pred = mkNomEqPred fam_app new_ty
    2391 
    +        given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note
    2360 2392
    2361 
    -----------------------
    2362 
    -swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
    2363 
    -              -> TcType -> CanEqLHS      -- ty ~ F tys
    2364 
    -              -> TcS (StopOrContinue (Either unused EqCt))
    2365 
    --- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
    2366 
    --- mentions alpha, it would not be a canonical constraint as-is.
    2367 
    --- We want to flip it to (F tys ~ a), whereupon it is canonical
    2368 
    -swapAndFinish ev eq_rel swapped lhs_ty can_rhs
    2369 
    -  = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty
    2370 
    -       ; continueWith $ Right $
    2371 
    -         EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
    2372 
    -              , eq_lhs = can_rhs, eq_rhs = lhs_ty } }
    2393 
    +    -- See Detail (7) of the Note
    2394 
    +    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
    2373 2395
    2374 2396 
     ----------------------
    2375 
    -tryIrredInstead :: CheckTyEqResult -> CtEvidence
    2376 
    -                -> EqRel -> SwapFlag -> CanEqLHS -> TcType
    2377 
    -                -> TcS (StopOrContinue (Either IrredCt unused))
    2378 
    --- We have a non-canonical equality
    2379 
    --- We still swap it if 'swapped' says so, so that it is oriented
    2380 
    --- in the direction that the error-reporting machinery
    2381 
    --- expects it; e.g.  (m ~ t m) rather than (t m ~ m)
    2382 
    --- This is not very important, and only affects error reporting.
    2383 
    -tryIrredInstead reason ev eq_rel swapped lhs rhs
    2384 
    -  = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
    2385 
    -       ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
    2386 
    -       ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
    2387 
    -
    2388 2397 
     finishCanWithIrred :: CtIrredReason -> CtEvidence
    2389 2398 
                        -> TcS (StopOrContinue (Either IrredCt a))
    2390 2399 
     finishCanWithIrred reason ev
    ... ... @@ -2404,8 +2413,63 @@ canEqReflexive ev eq_rel ty
    2404 2413 
       = do { setEqIfWanted ev (mkReflCPH eq_rel ty)
    2405 2414 
            ; stopWith ev "Solved by reflexivity" }
    2406 2415
    2407 
    -{- Note [Equalities with heterogeneous kinds]
    2408 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2416 
    +{- Note [Equalities where unification fails]
    2417 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2418 
    +If we can't unify, but the equality is canonical, we still want to add it to the
    2419 
    +inert set so that it can be used to rewrite other Wanteds.  (There are many
    2420 
    +reasons that unification might not happen: the LHS is not a touchable unification
    2421 
    +variable, it has rewriters, it's a Given etc.)
    2422 
    +
    2423 
    +* In this case we call `checkTypeEqNoUnification` to see whether it is canonical
    2424 
    +  (which in turn calls `checkTypeEqRhs` with suitable flags).
    2425 
    +
    2426 
    +* NB: we do /not/ try to take advantage of the case where
    2427 
    +  `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so
    2428 
    +  caused #27844.  (The first call did fam-app breaking, which concealed a genuine
    2429 
    +  occurs check.)  It's just too clever; better to do the simple thing.
    2430 
    +
    2431 
    +Note [Don't cycle-break Wanteds when not unifying]
    2432 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2433 
    +Consider
    2434 
    +  [W] a[2] ~ Maybe (F a[2])
    2435 
    +
    2436 
    +Should we cycle-break this Wanted, thus?
    2437 
    +
    2438 
    +  [W] a[2] ~ Maybe delta[2]
    2439 
    +  [W] delta[2] ~ F a[2]
    2440 
    +
    2441 
    +For a start, this is dodgy because we might just unify delta, thus undoing
    2442 
    +what we have done, and getting an infinite loop in the solver.  Even if we
    2443 
    +somehow prevented ourselves from doing so, is there any merit in the split?
    2444 
    +Maybe: perhaps we can use that equality on `a` to unlock other constraints?
    2445 
    +Consider
    2446 
    +  type instance F (Maybe _) = Bool
    2447 
    +
    2448 
    +  [G] g1: a ~ Maybe Bool
    2449 
    +  [W] w1: a ~ Maybe (F a)
    2450 
    +
    2451 
    +If we loop-break w1 to get
    2452 
    +  [W] w1': a ~ Maybe gamma
    2453 
    +  [W] w3:  gamma ~ F a
    2454 
    +Now rewrite w3 with w1'
    2455 
    +  [W] w3':  gamma ~ F (Maybe gamma)
    2456 
    +Now use the type instance to get
    2457 
    +  gamma := Bool
    2458 
    +Now we are left with
    2459 
    +  [W] w1': a ~ Maybe Bool
    2460 
    +which we can solve from the Given.
    2461 
    +
    2462 
    +BUT in this situation we could have rewritten the
    2463 
    +/original/ Wanted from the Given, like this:
    2464 
    +  [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
    2465 
    +and that is readily soluble.
    2466 
    +
    2467 
    +In short: loop-breaking Wanteds, when we aren't unifying,
    2468 
    +seems of no merit.  Hence TEFA_Recurse, rather than TEFA_Break,
    2469 
    +in `wanted_flags` in `checkTypeEqNoUnification`.
    2470 
    +
    2471 
    +Note [Equalities with heterogeneous kinds]
    2472 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2409 2473 
     What do we do when we have an equality
    2410 2474
    2411 2475 
       (tv :: k1) ~ (rhs :: k2)
    ... ... @@ -2587,8 +2651,8 @@ The details depend on whether we're working with a Given or a Wanted.
    2587 2651 
     Given
    2588 2652 
     -----
    2589 2653 
     We emit a new Given, [G] F a ~ cbv, equating the type family application
    2590 
    -to our new cbv. This is actually done by `break_given` in
    2591 
    -`GHC.Tc.Solver.Monad.checkTypeEq`.
    2654 
    +to our new cbv. This is actually done by `BreakGiven` in the `given_flags`
    2655 
    +in `checkTypeEqNoUnification`.
    2592 2656
    2593 2657 
     Note its orientation: The type family ends up on the left; see
    2594 2658 
     Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
    ... ... @@ -2629,7 +2693,7 @@ Note that
    2629 2693 
     Wanted
    2630 2694 
     ------
    2631 2695 
     First, we do not cycle-break unless the LHS is a unifiable type variable
    2632 
    -See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad.
    2696 
    +See Note [Don't cycle-break Wanteds when not unifying].
    2633 2697
    2634 2698 
     OK, so suppose the LHS is a unifiable type variable.  The fresh cycle-breaker
    2635 2699 
     variables here must actually be normal, touchable metavariables. That is, they
    ... ... @@ -3073,11 +3137,10 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w
    3073 3137 
           || (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i)))
    3074 3138 
                  -- Prefer the one that has no rewriters
    3075 3139 
                  -- See (CE4) in Note [Combining equalities]
    3140 
    +             -- and (WRW10) in Note [Wanteds rewrite Wanteds: rewriter-sets]
    3076 3141
    3077 3142 
     inertsEqsCanDischarge _ _ = Nothing
    3078 3143
    3079 
    -
    3080 
    -
    3081 3144 
     {- Note [Do not unify Givens]
    3082 3145 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    3083 3146 
     Consider this GADT match
    ... ... @@ -3143,34 +3206,6 @@ Wrinkles:
    3143 3206 
        we should kick out `co` so that we can now unify it, which might
    3144 3207 
        unlock other stuff.  See `kickOutAfterFillingCoercionHole` in
    3145 3208 
        GHC.Tc.Solver.Monad.
    3146 
    -
    3147 
    -Note [Solve by unification]
    3148 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~
    3149 
    -If we solve
    3150 
    -   alpha[n] ~ ty
    3151 
    -by unification, there are two cases to consider
    3152 
    -
    3153 
    -* TouchableSameLevel: if the ambient level is 'n', then
    3154 
    -  we can simply update alpha := ty, and do nothing else
    3155 
    -
    3156 
    -* TouchableOuterLevel free_metas n: if the ambient level is greater than
    3157 
    -  'n' (the level of alpha), in addition to setting alpha := ty we must
    3158 
    -  do two other things:
    3159 
    -
    3160 
    -  1. Promote all the free meta-vars of 'ty' to level n.  After all,
    3161 
    -     alpha[n] is at level n, and so if we set, say,
    3162 
    -          alpha[n] := Maybe beta[m],
    3163 
    -     we must ensure that when unifying beta we do skolem-escape checks
    3164 
    -     etc relevant to level n.  Simple way to do that: promote beta to
    3165 
    -     level n.
    3166 
    -
    3167 
    -  2. Set the Unification Level Flag to record that a level-n unification has
    3168 
    -     taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify
    3169 
    -
    3170 
    -NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion
    3171 
    -would be a no-op, and setting the unification flag unnecessarily would just
    3172 
    -make the solver iterate more often.  (We don't need to iterate when unifying
    3173 
    -at the ambient level because of the kick-out mechanism.)
    3174 3209 
     -}
    3175 3210
    3176 3211

  • compiler/GHC/Tc/Solver/InertSet.hs
    ... ... @@ -22,7 +22,7 @@ module GHC.Tc.Solver.InertSet (
    22 22 
         InertEqs,
    23 23 
         foldTyEqs, delEq, findEq,
    24 24 
         partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs,
    25 
    -    filterInertEqs, filterFunEqs,
    25 
    +    filterInertEqs, filterFunEqs, transformAndPartitionFunEqs,
    26 26 
         foldFunEqs, addEqToCans,
    27 27
    28 28 
         -- * Inert Dicts
    ... ... @@ -128,7 +128,7 @@ Further refinements:
    128 128
    129 129 
     * Among the equalities we prioritise ones with an empty rewriter set;
    130 130 
       see Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint,
    131 
    -  wrinkle (WRW8).
    131 
    +  wrinkle (WRW7).
    132 132
    133 133 
     * Among equalities with an empty rewriter set, we prioritise nominal equalities.
    134 134 
        * They have more rewriting power, so doing them first is better.
    ... ... @@ -983,7 +983,7 @@ How do we establish these conditions?
    983 983 
         with S(fw,_).
    984 984
    985 985 
       * (T3) is guaranteed by an occurs-check on the work item.
    986 
    -    This is done during canonicalisation, in checkTypeEq; invariant
    986 
    +    This is done during canonicalisation, in checkTyEqRhs; invariant
    987 987 
         (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
    988 988
    989 989 
       * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable.  If the inert
    ... ... @@ -1422,6 +1422,19 @@ addCanFunEq old_eqs fun_tc fun_args ct
    1422 1422 
     foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
    1423 1423 
     foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z
    1424 1424
    1425 
    +transformAndPartitionFunEqs
    1426 
    +  :: (EqCt -> Either EqCt EqCt)         -- Left => chuck out, Right => keep
    1427 
    +  -> InertFunEqs
    1428 
    +  -> ([EqCt], InertFunEqs)               -- (chuck-out, keep)
    1429 
    +transformAndPartitionFunEqs pred orig_inerts
    1430 
    +  = foldFunEqs folder orig_inerts ([], emptyFunEqs)
    1431 
    +  where
    1432 
    +    folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs)
    1433 
    +    folder eq_ct (acc_true, acc_false)
    1434 
    +      = case pred eq_ct of
    1435 
    +           Left eq_ct'  -> (eq_ct' : acc_true, acc_false)
    1436 
    +           Right eq_ct' -> (acc_true, addFunEqs eq_ct' acc_false)
    1437 
    +
    1425 1438 
     partitionFunEqs :: (EqCt -> Bool)    -- EqCt will have a TyFamLHS
    1426 1439 
                     -> InertFunEqs
    1427 1440 
                     -> ([EqCt], InertFunEqs)

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad (
    117 117 
         getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
    118 118 
         matchFam, matchFamTcM,
    119 119 
         checkWellLevelledDFun,
    120 
    -    pprEq,
    121 
    -
    122 
    -    -- Enforcing invariants for type equalities
    123 
    -    checkTypeEq
    120 
    +    pprEq
    124 121 
     ) where
    125 122
    126 123 
     import GHC.Prelude
    ... ... @@ -436,32 +433,48 @@ we should kick out `co` so that we can now unify it, which might unlock other st
    436 433 
     See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for
    437 434 
     why solving `kco` might unlock `co`, especially (URW2).
    438 435
    439 
    -Hence `kickOutAfterFillingCoercionHole`.  It looks at inert constraints that are
    436 
    +Hence `kickOutAfterFillingCoercionHole`.  It looks at inert constraints
    437 
    +           [W] co :: ty1 ~ tys
    438 
    +that are
    440 439 
       * Wanted
    441 
    -  * Of the form  alpha ~ rhs, where alpha is a unification variable
    442 
    -and kicks out any that will have an empty rewriter set after filling the hole.
    440 
    +  * Of the form  (alpha ~ rhs)
    441 
    +             or  (F tys ~ alpha)
    442 
    +             or  (F tys ~ alpha |> co)
    443 
    +    where alpha is a unification variable
    444 
    + and kicks out any that have an empty rewriter set after filling the hole.
    443 445
    444 446 
     Wrinkles:
    447 
    +
    445 448 
     (KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out,
    446 449 
            because it still can't be unified.  So we only kick out if the co's
    447 450 
            rewriter-set becomes empty.
    448 451
    449 
    -(KOC2) `kco` might itself have a rewriter set.  This is fairly common.  E.g.
    452 
    +(KOC2) `kco` might itself have been rewritten by other as-yet-unsolved new_holes.
    453 
    +       This is fairly common.  E.g.
    450 454 
                    kco : a[sk] ~ beta[tau]
    451 455 
            Assuming we can't unify it for some reason, we may swap that over to give
    452 456 
                    kco2 : beta[tau] ~ a[sk]      kco := sym kco2
    453 457 
            So `kco` is "solved" but the coercion that solves it has free coercion holes!
    454 458 
            So rather than kick out `co`, we should just change its rewriter-set to depend
    455 
    -       on `kco2` instead of `kco`.  Hence the `new_holes` passed to
    456 
    -       `kickOutAfterFillingCoercionHole`
    459 
    +       on `kco2` instead of `kco`.
    457 460
    458 
    -(KOC3) It's possible that this could just go ahead and unify, but could there
    459 
    -       be occurs-check problems? Seems simpler just to kick out.
    461 
    +       Hence the `new_holes` passed to `kickOutAfterFillingCoercionHole`
    462 
    +
    463 
    +(KOC3) It's possible that this could just go ahead and unify on the spot, but could
    464 
    +       there be occurs-check problems? Seems simpler just to kick out.
    460 465
    461 466 
     (KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`.  So
    462 467 
            the solver prioritises equalities with an empty rewriter set, to try to
    463 468 
            avoid unnecessary kick-out.  See GHC.Tc.Types.Constraint
    464 469 
            Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1)
    470 
    +
    471 
    +(KOC5) We kick out from both `inert_eqs` and `inert_funeqs`.  The latter is needed
    472 
    +       in case we have (F tys ~ alpha), which might (if it now has an empty rewriter
    473 
    +       set) allow unifying alpha.
    474 
    +
    475 
    +(KOC6) Annoyingly, we /also/ need to look for (F tys ~ (alpha |> co)), with a cast,
    476 
    +       because that may be unifiable by moving the cast to the other side.  Hence
    477 
    +       `getCastedTyVar_maybe`.
    465 478 
     -}
    466 479
    467 480 
     kickOutRewritable  :: KickOutSpec -> CtFlavourRole -> TcS ()
    ... ... @@ -526,27 +539,36 @@ kickOutAfterFillingCoercionHole hole (CPH { cph_holes = new_holes })
    526 539 
            ; setInertCans ics' }
    527 540 
       where
    528 541 
         kick_out :: InertCans -> ([EqCt], InertCans)
    529 
    -    kick_out ics@(IC { inert_eqs = eqs })
    530 
    -      = (eqs_to_kick, ics { inert_eqs = eqs_to_keep })
    542 
    +    kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
    543 
    +      = ( kick_funeqs ++ kick_eqs
    544 
    +        , ics { inert_eqs = keep_eqs, inert_funeqs = keep_funeqs })
    531 545 
           where
    532 
    -        (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs
    546 
    +        (kick_eqs,       keep_eqs) = transformAndPartitionTyVarEqs kick_out_eq eqs
    547 
    +        (kick_funeqs, keep_funeqs) = transformAndPartitionFunEqs   kick_out_eq funeqs
    548 
    +        -- Kick out from funeqs as well as eqs.
    549 
    +        -- See (KOC5) in Note [Kick out after filling a coercion hole]
    533 550
    534 551 
         kick_out_eq :: EqCt -> Either EqCt EqCt
    535 
    -    kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs })
    552 
    +    kick_out_eq eq_ct@(EqCt { eq_ev = ev })
    536 553 
           | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev
    537 
    -      , TyVarLHS tv <- lhs
    538 
    -      , isMetaTyVar tv
    539 554 
           , hole `elemCoHoleSet` rewriters
    540 
    -      , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
    541 
    -                     -- Adding new_holes and deleting hole: see (KOC2)
    542 
    -            eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }
    543 
    -      = if isEmptyCoHoleSet holes'
    555 
    +      , is_meta_tv_equality eq_ct
    556 
    +      , let rewriters' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
    557 
    +                         -- Adding new_holes and deleting hole: see (KOC2)
    558 
    +            eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = rewriters' }) }
    559 
    +      = if isEmptyCoHoleSet rewriters'
    544 560 
             then Left eq_ct'    -- Kick out, if new rewriter set is empty (KOC1)
    545 561 
             else Right eq_ct'   -- Keep, but with trimmed holes see (KOC2)
    562 
    +
    546 563 
           | otherwise
    547 564 
           = Right eq_ct
    548 565
    549 
    ---------------
    566 
    +    is_meta_tv_equality (EqCt { eq_lhs = lhs, eq_rhs = rhs })
    567 
    +       | TyVarLHS tv <- lhs                      = isMetaTyVar tv
    568 
    +       | Just (tv,_) <- getCastedTyVar_maybe rhs = isMetaTyVar tv
    569 
    +       | otherwise                               = False
    570 
    +       -- getCastedTyVar: see (KOC5) in Note [Kick out after filling a coercion hole]
    571 
    +
    550 572 
     insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
    551 573 
     -- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
    552 574 
     insertSafeOverlapFailureTcS what item
    ... ... @@ -2302,52 +2324,6 @@ wrapUnifier rws loc role do_unifications
    2302 2324 
     ************************************************************************
    2303 2325 
     -}
    2304 2326
    2305 
    -checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
    2306 
    -            -> TcS (PuResult Ct Reduction)
    2307 
    --- Used for general CanEqLHSs, ones that do
    2308 
    --- not have a touchable type variable on the LHS (i.e. not unifying)
    2309 
    -checkTypeEq ev eq_rel lhs rhs =
    2310 
    -  case ev of
    2311 
    -    CtGiven {} ->
    2312 
    -      do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
    2313 
    -                                          , text "rhs:" <+> ppr rhs ])
    2314 
    -         ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
    2315 
    -         ; traceTcS "checkTypeEq }" (ppr check_result)
    2316 
    -         ; case check_result of
    2317 
    -              PuFail reason -> return (PuFail reason)
    2318 
    -              PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
    2319 
    -                                  ; emitWork new_givens
    2320 
    -                                  ; updInertSet (addCycleBreakerBindings prs)
    2321 
    -                                  ; return (pure redn) } }
    2322 
    -    CtWanted {} -> wrapTcS (checkTyEqRhs wanted_flags rhs)
    2323 
    -  where
    2324 
    -    wanted_flags :: TyEqFlags TcM Ct
    2325 
    -    wanted_flags = notUnifying_TEFTask occ_prob lhs
    2326 
    -                   -- checkTypeEq deals only with the non-unifying case
    2327 
    -
    2328 
    -    given_flags :: TyEqFlags TcM (TcTyVar, TcType)
    2329 
    -    given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
    2330 
    -        -- TEFA_Break used for: [G] a ~ Maybe (F a)
    2331 
    -        --                   or [W] F a ~ Maybe (F a)
    2332 
    -
    2333 
    -    -- occ_prob: see Note [Occurs check and representational equality]
    2334 
    -    occ_prob = case eq_rel of
    2335 
    -                 NomEq  -> cteInsolubleOccurs
    2336 
    -                 ReprEq -> cteSolubleOccurs
    2337 
    -
    2338 
    -    ---------------------------
    2339 
    -    mk_new_given :: (TcTyVar, TcType) -> TcS Ct
    2340 
    -    mk_new_given (new_tv, fam_app)
    2341 
    -      = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
    2342 
    -      where
    2343 
    -        new_ty     = mkTyVarTy new_tv
    2344 
    -        given_pred = mkNomEqPred fam_app new_ty
    2345 
    -        given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note
    2346 
    -
    2347 
    -    -- See Detail (7) of the Note
    2348 
    -    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
    2349 
    -
    2350 
    --------------------------
    2351 2327 
     -- | Fill in CycleBreakerTvs with the variables they stand for.
    2352 2328 
     -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
    2353 2329 
     restoreTyVarCycles :: InertSet -> TcM ()
    ... ... @@ -2363,43 +2339,4 @@ restoreTyVarCycles is
    2363 2339 
     (a ~R# b a) is soluble if b later turns out to be Identity
    2364 2340 
     So we treat this as a "soluble occurs check".
    2365 2341
    2366 
    -Note [Don't cycle-break Wanteds when not unifying]
    2367 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2368 
    -Consdier
    2369 
    -  [W] a[2] ~ Maybe (F a[2])
    2370 
    -
    2371 
    -Should we cycle-break this Wanted, thus?
    2372 
    -
    2373 
    -  [W] a[2] ~ Maybe delta[2]
    2374 
    -  [W] delta[2] ~ F a[2]
    2375 
    -
    2376 
    -For a start, this is dodgy because we might just unify delta, thus undoing
    2377 
    -what we have done, and getting an infinite loop in the solver.  Even if we
    2378 
    -somehow prevented ourselves from doing so, is there any merit in the split?
    2379 
    -Maybe: perhaps we can use that equality on `a` to unlock other constraints?
    2380 
    -Consider
    2381 
    -  type instance F (Maybe _) = Bool
    2382 
    -
    2383 
    -  [G] g1: a ~ Maybe Bool
    2384 
    -  [W] w1: a ~ Maybe (F a)
    2385 
    -
    2386 
    -If we loop-break w1 to get
    2387 
    -  [W] w1': a ~ Maybe gamma
    2388 
    -  [W] w3:  gamma ~ F a
    2389 
    -Now rewrite w3 with w1'
    2390 
    -  [W] w3':  gamma ~ F (Maybe gamma)
    2391 
    -Now use the type instance to get
    2392 
    -  gamma := Bool
    2393 
    -Now we are left with
    2394 
    -  [W] w1': a ~ Maybe Bool
    2395 
    -which we can solve from the Given.
    2396 
    -
    2397 
    -BUT in this situation we could have rewritten the
    2398 
    -/original/ Wanted from the Given, like this:
    2399 
    -  [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
    2400 
    -and that is readily soluble.
    2401 
    -
    2402 
    -In short: loop-breaking Wanteds, when we aren't unifying,
    2403 
    -seems of no merit.  Hence TEFA_Recurse, rather than TEFA_Break,
    2404 
    -in `wanted_flags` in `checkTypeEq`.
    2405 2342 
     -}

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True
    524 524 
     ------------------------------------------------------------------------------
    525 525
    526 526 
     -- | A /set/ of problems in checking the validity of a type equality.
    527 
    --- See 'checkTypeEq'.
    527 
    +-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'.
    528 528 
     newtype CheckTyEqResult = CTER Word8
    529 529
    530 530 
     -- | No problems in checking the validity of a type equality.
    ... ... @@ -2603,19 +2603,24 @@ The rewriter-set plan
    2603 2603 
        thereby dropping the reference to `co`.  I'm not certain whether this actually
    2604 2604 
        happens or not.
    2605 2605
    2606 
    -(WRW7) In error reporting, we simply suppress any errors that have been rewritten
    2607 
    -  by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
    2606 
    +(WRW7) When we fill a coercion hole `h` we kick out any inert Wanted that has `h`
    2607 
    +   in its rewriter set.  See `kickOutAfterFilling CoercionHole`.
    2608 
    +   See Note [Kick out after filling a coercion hole] in GHC.Tc.Solver.Monad.
    2609 
    +
    2610 
    +   Furthermore, when we select a work item, in `selectNextWorkItem` we zonk the
    2611 
    +   rewriter set so that it accurately reflects the unsolved coercion holes. That
    2612 
    +   sets it up ready for the no-rewriter check in (WR5), when we process the equality.
    2613 
    +
    2614 
    +   In `selectNextWorkItem`, we also prioritise equalities with no rewiters.
    2615 
    +   See Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
    2616 
    +   wrinkle (PER1).
    2617 
    +
    2618 
    +(WRW8) In error reporting, we suppress any errors that have been rewritten
    2619 
    +  by /unsolved/ wanteds. This suppression happens in `GHC.Tc.Errors.mkErrorItem`,
    2608 2620 
       which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` to look through any filled
    2609 2621 
       coercion holes. The idea is that we wish to report the "root cause" -- the
    2610 2622 
       error that rewrote all the others.
    2611 2623
    2612 
    -(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters.  See
    2613 
    -  Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
    2614 
    -  wrinkle (PER1).
    2615 
    -
    2616 
    -(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet:
    2617 
    -  see Note [Prioritise Wanteds with empty CoHoleSet].
    2618 
    -
    2619 2624 
     Let's continue our first example above:
    2620 2625
    2621 2626 
       inert: [W] w1 :: a ~ Char
    ... ... @@ -2641,8 +2646,10 @@ Wrinkles:
    2641 2646
    2642 2647 
     (WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take
    2643 2648 
        the opportunity to zonk its `CoHoleSet`, which eliminates solved ones.
    2644 
    -   This doesn't guarantee that rewriter sets are always up to date -- c.f.
    2645 
    -   (WRW10) -- but it helps, and it de-clutters debug output.
    2649 
    +   This doesn't guarantee that rewriter sets are always up to date (c.f. (WRW10))
    2650 
    +   but it helps, and it de-clutters debug output.
    2651 
    +
    2652 
    +   See also (WRW7) which does the crucial just-in-time zonking of the rewriters.
    2646 2653
    2647 2654 
     Note [Prioritise Wanteds with empty CoHoleSet]
    2648 2655 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -2685,9 +2692,8 @@ in our simplify_loop iteration, we happened to start with co_aym. All would have
    2685 2692 
     been well if we'd started with the (not-rewritten) co_ayb and gotten it into the
    2686 2693 
     inert set.
    2687 2694
    2688 
    -With that in mind, we /prioritise/ the work-list to put
    2689 
    -constraints with no rewriters first.  This prioritisation
    2690 
    -is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
    2695 
    +With that in mind, we /prioritise/ the work-list to put constraints with no rewriters
    2696 
    +first.  This prioritisation is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
    2691 2697
    2692 2698 
     Wrinkles
    2693 2699
    ... ... @@ -2700,8 +2706,8 @@ Wrinkles
    2700 2706 
       order to report /some/ error in this case, we simply report all the
    2701 2707 
       Wanteds. The user will get a perhaps-confusing error message, but they've
    2702 2708 
       written a confusing program!  (T22707 and T22793 were close, but they do
    2703 
    -  not exhibit this behaviour.)  So belt and braces: see the `suppress`
    2704 
    -  stuff in GHC.Tc.Errors.mkErrorItem.
    2709 
    +  not exhibit this behaviour.)  So belt and braces:
    2710 
    +  see `GHC.Tc.Errors.reportWanteds`.
    2705 2711
    2706 2712 
     Note [Avoiding rewriting cycles]
    2707 2713 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -3617,15 +3617,20 @@ instance Outputable SimpleUnifyResult where
    3617 3617 
     simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult
    3618 3618 
     -- ^ A fast check for unification. May return "not sure", in which case
    3619 3619 
     -- unification might still be OK, but it'll take more work to do
    3620 
    --- (use the full 'checkTypeEq').
    3620 
    +-- (use the full 'checkTyEqRhs').
    3621 3621 
     --
    3622 
    --- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
    3623 
    --- * Rejects foralls unless
    3624 
    ---      lhs_tv is RuntimeUnk (used by GHCi debugger)
    3625 
    ---          or is a QL instantiation variable
    3626 
    --- * Rejects a non-concrete type if lhs_tv is concrete
    3627 
    --- * Rejects type families unless fam_ok=True
    3628 
    --- * Does a level-check for type variables, to avoid skolem escape
    3622 
    +-- It returns SUC_CannotUnify for
    3623 
    +--   * Touchability failure
    3624 
    +--   * Top level-shape failure
    3625 
    +--
    3626 
    +-- It returns SUC_NotSure for
    3627 
    +--   * Occurs check: lhs_tv occurs in rhs_ty
    3628 
    +--   * Type families unless fam_ok=True
    3629 
    +--   * Foralls unless
    3630 
    +--        lhs_tv is RuntimeUnk (used by GHCi debugger)
    3631 
    +--            or is a QL instantiation variable
    3632 
    +--   * Concreteness: lhs_tv is concrete and rhs is a non-concrete type
    3633 
    +--   * Skolem-escape: a level-check for type variables, to avoid skolem escape
    3629 3634 
     --
    3630 3635 
     -- This function is pretty heavily used, so it's optimised not to allocate
    3631 3636 
     simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
    ... ... @@ -3753,8 +3758,8 @@ Consider
    3753 3758 
        [W] alpha[2] ~ Maybe (S beta[4] gamma[2])
    3754 3759
    3755 3760 
     We don't want to promote beta to level 2; rather, we should
    3756 
    -expand the synonym. (Currently, in checkTypeEqRhs promotion
    3757 
    -is irrevocable, by side effect.)
    3761 
    +expand the synonym. (Currently, in `checkTyEqRhs` promotion
    3762 
    +is irrevocable, by side effect in `promote` in `checkTyVar`.)
    3758 3763
    3759 3764 
     To avoid this risk we eagerly expand forgetful synonyms.
    3760 3765 
     This also means we won't get an occurs check in
    ... ... @@ -4198,7 +4203,7 @@ famAppArgFlags flags = case flags of
    4198 4203 
     The key function `checkTyEqRhs ty_eq_flags rhs` is called on the
    4199 4204 
     RHS of a type equality
    4200 4205 
            lhs ~ rhs
    4201 
    -and checks to see if `rhs` satisfies, or can be made to satisfy,
    4206 
    +and checks to see if `rhs` satisfies, /or can be made to satisfy/,
    4202 4207 
     invariants described by `ty_eq_flags`.  It can succeded or fail; in
    4203 4208 
     the latter case it returns a `CheckTyEqResult` that describes why it
    4204 4209 
     failed.
    ... ... @@ -4219,6 +4224,15 @@ Notably, it can check for things like:
    4219 4224 
       * Concreteness error
    4220 4225 
           e.g. alpha[conc] ~ r[sk]
    4221 4226
    4227 
    +Note "or can be made to satisfy the preconditions"!  `checkTyEqRhs` may transform
    4228 
    +the RHS by
    4229 
    +
    4230 
    +  * Turning a type-family application into a type variable, perhaps to avoid
    4231 
    +    an occurs check.  See Note Note [Family applications in canonical constraints]
    4232 
    +
    4233 
    +  * Promoting any nested unification variables, in order to satisfy the
    4234 
    +    level invariant. See Note [Promotion and level-checking]
    4235 
    +
    4222 4236 
     Its specific behaviour is governed by the `TyEqFlags` that are passed
    4223 4237 
     to it; see Note [TyEqFlags].
    4224 4238
    ... ... @@ -4275,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as
    4275 4289 
         [G] a ~ F tys here
    4276 4290 
     because we'd have swapped it to
    4277 4291 
        [G] F tys ~ a
    4278 
    -in canEqCanLHS2, before getting to checkTypeEq.
    4292 
    +in canEqCanLHS2, before getting to checkTyEqRhs.
    4279 4293 
     -}
    4280 4294
    4281 4295 
     check_ty_eq_rhs :: forall m a
    ... ... @@ -4799,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv
    4799 4813 
     touchabilityTest :: TcLevel -> TcTyVar -> Bool
    4800 4814 
     -- ^ This is the key test for untouchability:
    4801 4815 
     -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
    4802 4816 
     --
    4803 4817 
     -- @True@ <=> the variable is touchable
    4804 4818 
     touchabilityTest given_eq_lvl tv

  • testsuite/tests/indexed-types/should_fail/T9662.stderr
    1 1 
     T9662.hs:49:8: error: [GHC-25897]
    2 
    -    • Couldn't match type ‘n’ with ‘Int’
    2 
    +    • Couldn't match type ‘m’ with ‘Int’
    3 3 
           Expected: Exp (((sh :. k) :. m) :. n)
    4 4 
                     -> Exp (((sh :. m) :. n) :. k)
    5 5 
             Actual: Exp
    6 6 
                       (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
    7 7 
                     -> Exp
    8 8 
                          (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
    9 
    -      ‘n’ is a rigid type variable bound by
    9 
    +      ‘m’ is a rigid type variable bound by
    10 10 
             the type signature for:
    11 11 
               test :: forall sh k m n.
    12 12 
                       Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)

  • testsuite/tests/typecheck/should_fail/T12785b.stderr
    1 
    -
    2 1 
     T12785b.hs:30:65: error: [GHC-25897]
    3 
    -    • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’
    2 
    +    • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’
    4 3 
             arising from a use of ‘SBranchX’
    5 4 
           from the context: m ~ S n
    6 5 
             bound by a pattern with constructor:
    ... ... @@ -25,3 +24,4 @@ T12785b.hs:30:65: error: [GHC-25897]
    25 24 
             a :: STree (S m) f s (bound at T12785b.hs:30:12)
    26 25 
             nest :: HTree m (Hidden (S m) f) -> Hidden m (STree (S m) f)
    27 26 
               (bound at T12785b.hs:28:1)
    27 
    +

  • testsuite/tests/typecheck/should_fail/T27844.hs
    1 
    +-- Repro.hs
    2 
    +-- The call to f forces c ~ (b, F c) inside the scope of the skolem b.
    3 
    +-- Correct behaviour: a type error at the first argument of const
    4 
    +-- (as GHC 9.12.4 reports).
    5 
    +
    6 
    +{-# LANGUAGE RankNTypes, TypeFamilies #-}
    7 
    +module T27844 where
    8 
    +
    9 
    +type family F a
    10 
    +
    11 
    +f :: (forall b. b -> (b, F c)) -> c -> ()
    12 
    +f _ _ = ()
    13 
    +
    14 
    +g x = f (\_ -> const x (show x)) x

  • testsuite/tests/typecheck/should_fail/T27844.stderr
    1 
    +T27844.hs:14:22: error: [GHC-25897]
    2 
    +    • Couldn't match expected type ‘(b, F c)’ with actual type ‘c’
    3 
    +      ‘c’ is a rigid type variable bound by
    4 
    +        the inferred type of g :: Show c => c -> ()
    5 
    +        at T27844.hs:14:1-34
    6 
    +    • In the first argument of ‘const’, namely ‘x’
    7 
    +      In the expression: const x (show x)
    8 
    +      In the first argument of ‘f’, namely ‘(\ _ -> const x (show x))’
    9 
    +    • Relevant bindings include
    10 
    +        x :: c (bound at T27844.hs:14:3)
    11 
    +        g :: c -> () (bound at T27844.hs:14:1)
    12 
    +

  • testsuite/tests/typecheck/should_fail/all.T
    ... ... @@ -766,3 +766,5 @@ test('T26862', normal, compile_fail, [''])
    766 766 
     test('T27210', normal, compile_fail, [''])
    767 767 
     test('T26532', normal, compile_fail, [''])
    768 768 
     test('T27731', normal, compile_fail, [''])
    769 
    +test('T27844', normal, compile_fail, [''])
    770 
    +

    • —
    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/7807b4d3ef52aa36b42b39c58d7cafa8ba889cd2 at 1791820943