Magnus pushed to branch ghc-9.12 at Glasgow Haskell Compiler / GHC

Commits:

12 changed files:

Changes:

  • compiler/GHC/Tc/Gen/App.hs
    ... ... @@ -2038,22 +2038,22 @@ qlUnify ty1 ty2
    2038 2038 
           = go_flexi1 kappa ty2
    2039 2039
    2040 2040 
         go_flexi1 kappa ty2  -- ty2 is zonked
    2041 
    -      | -- See Note [QuickLook unification] (UQL1)
    2042 
    -        simpleUnifyCheck UC_QuickLook kappa ty2
    2043 
    -      , checkTopShape (metaTyVarInfo kappa) ty2
    2044 
    -          -- NB: don't forget to do a shape check, as we might be dealing
    2045 
    -          -- with an ordinary metavariable (and not a quick-look instantiation variable).
    2046 
    -          -- (Forgetting this led to #25950.)
    2047 
    -      = do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
    2048 
    -                   -- unifyKind: see (UQL2) in Note [QuickLook unification]
    2049 
    -                   --            and (MIV2) in Note [Monomorphise instantiation variables]
    2050 
    -           ; let ty2' = mkCastTy ty2 co
    2051 
    -           ; traceTc "qlUnify:update" $
    2052 
    -             ppr kappa <+> text ":=" <+> ppr ty2
    2053 
    -           ; liftZonkM $ writeMetaTyVar kappa ty2' }
    2054 
    -
    2055 
    -      | otherwise
    2056 
    -      = return ()   -- Occurs-check or forall-bound variable
    2041 
    +      = do { cur_lvl <- getTcLevel
    2042 
    +              -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
    2043 
    +              -- Here we are in the TcM monad, which does not track enclosing
    2044 
    +              -- Given equalities; so for quick-look unification we conservatively
    2045 
    +              -- treat /any/ level outside this one as untouchable. Hence cur_lvl.
    2046 
    +           ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of
    2047 
    +              SUC_CanUnify ->
    2048 
    +                do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
    2049 
    +                           -- unifyKind: see (UQL2) in Note [QuickLook unification]
    2050 
    +                           --            and (MIV2) in Note [Monomorphise instantiation variables]
    2051 
    +                   ; let ty2' = mkCastTy ty2 co
    2052 
    +                   ; traceTc "qlUnify:update" $
    2053 
    +                     ppr kappa <+> text ":=" <+> ppr ty2
    2054 
    +                   ; liftZonkM $ writeMetaTyVar kappa ty2' }
    2055 
    +              _ -> return () -- e.g. occurs-check or forall-bound variable
    2056 
    +           }
    2057 2057 
           where
    2058 2058 
             kappa_kind = tyVarKind kappa
    2059 2059 
             ty2_kind   = typeKind ty2

  • compiler/GHC/Tc/Solver/Equality.hs
    1 1 
     {-# LANGUAGE CPP #-}
    2 
    +{-# LANGUAGE DuplicateRecordFields #-}
    3 
    +{-# LANGUAGE LambdaCase #-}
    2 4 
     {-# LANGUAGE MultiWayIf #-}
    3 5
    4 6 
     module GHC.Tc.Solver.Equality(
    ... ... @@ -1884,83 +1886,104 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
    1884 1886 
     -----------------------
    1885 1887 
     canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    1886 1888 
       -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
    1887 
    -  | isWanted ev      -- See Note [Do not unify Givens]
    1888 
    -  , NomEq <- eq_rel  -- See Note [Do not unify representational equalities]
    1889 
    -  , TyVarLHS tv <- lhs
    1890 
    -  = do { given_eq_lvl <- getInnermostGivenEqLevel
    1891 
    -       ; if not (touchabilityAndShapeTest given_eq_lvl tv rhs)
    1892 
    -         then if | Just can_rhs <- canTyFamEqLHS_maybe rhs
    1893 
    -                 -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
    1894 
    -                    -- See Note [Orienting TyVarLHS/TyFamLHS]
    1895 
    -
    1896 
    -                 | otherwise
    1897 
    -                 -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    1898 
    -         else
    1899 
    -
    1900 
    -    -- We have a touchable unification variable on the left
    1901 
    -    do { check_result <- checkTouchableTyVarEq ev tv rhs
    1902 
    -       ; case check_result of {
    1903 
    -            PuFail reason
    1889 
    +  | isWanted ev         -- See Note [Do not unify Givens]
    1890 
    +  , NomEq <- eq_rel     -- See Note [Do not unify representational equalities]
    1891 
    +  , TyVarLHS lhs_tv <- lhs
    1892 
    +  = do  { given_eq_lvl <- getInnermostGivenEqLevel
    1893 
    +        ; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of
    1894 
    +            SUC_CanUnify ->
    1895 
    +              unify lhs_tv (mkReflRedn Nominal rhs)
    1896 
    +            SUC_CannotUnify
    1904 1897 
                   | Just can_rhs <- canTyFamEqLHS_maybe rhs
    1905 
    -              -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
    1906 
    -                -- Swap back: see Note [Orienting TyVarLHS/TyFamLHS]
    1907 
    -
    1908 
    -              | reason `cterHasOnlyProblems` do_not_prevent_rewriting
    1909 
    -              -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    1910 
    -
    1898 
    +              -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
    1911 1899 
                   | otherwise
    1912 
    -              -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
    1913 
    -
    1914 
    -            PuOK _ rhs_redn ->
    1915 
    -
    1916 
    -    -- Success: we can solve by unification
    1917 
    -    do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
    1918 
    -         -- the evidence, even if swapped=IsSwapped.   Suppose the original was
    1919 
    -         --     [W] co : Int ~ alpha
    1920 
    -         -- We unify alpha := Int, and set co := <Int>.  No need to
    1921 
    -         -- swap to   co = sym co'
    1922 
    -         --           co' = <Int>
    1923 
    -         new_ev <- if isReflCo (reductionCoercion rhs_redn)
    1924 
    -                   then return ev
    1925 
    -                   else rewriteEqEvidence emptyRewriterSet ev swapped
    1926 
    -                            (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
    1927 
    -
    1928 
    -       ; let tv_ty     = mkTyVarTy tv
    1929 
    -             final_rhs = reductionReducedType rhs_redn
    1930 
    -
    1931 
    -       ; traceTcS "Sneaky unification:" $
    1932 
    -         vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs,
    1933 
    -               text "Coercion:" <+> pprEq tv_ty final_rhs,
    1934 
    -               text "Left Kind is:" <+> ppr (typeKind tv_ty),
    1935 
    -               text "Right Kind is:" <+> ppr (typeKind final_rhs) ]
    1936 
    -
    1937 
    -       -- Update the unification variable itself
    1938 
    -       ; unifyTyVar tv final_rhs
    1939 
    -
    1940 
    -       -- Provide Refl evidence for the constraint
    1941 
    -       -- Ignore 'swapped' because it's Refl!
    1942 
    -       ; setEvBindIfWanted new_ev EvCanonical $
    1943 
    -         evCoercion (mkNomReflCo final_rhs)
    1944 
    -
    1945 
    -       -- Kick out any constraints that can now be rewritten
    1946 
    -       ; kickOutAfterUnification [tv]
    1947 
    -
    1948 
    -       ; return (Stop new_ev (text "Solved by unification")) }}}}
    1949 
    -
    1900 
    +              -> finish_no_unify
    1901 
    +            SUC_NotSure ->
    1902 
    +              -- We have a touchable unification variable on the left,
    1903 
    +              -- and the top-shape check succeeded. These are both guaranteed
    1904 
    +              -- by the fact that simpleUnifyCheck did not return SUC_CannotUnify.
    1905 
    +              do  { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv
    1906 
    +                  ; check_result <- wrapTcS (checkTyEqRhs flags rhs)
    1907 
    +                  ; case check_result of
    1908 
    +                      PuOK cts rhs_redn ->
    1909 
    +                        do { emitWork cts
    1910 
    +                           ; unify lhs_tv rhs_redn }
    1911 
    +                      PuFail reason
    1912 
    +                        | Just can_rhs <- canTyFamEqLHS_maybe rhs
    1913 
    +                        -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
    1914 
    +                        | reason `cterHasOnlyProblems` do_not_prevent_rewriting
    1915 
    +                        ->
    1916 
    +                          -- ContinueWith, to allow using this constraint for
    1917 
    +                          -- rewriting (e.g. alpha[2] ~ beta[3]).
    1918 
    +                          do { let role = eqRelRole eq_rel
    1919 
    +                             ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
    1920 
    +                                 (mkReflRedn role (canEqLHSType lhs))
    1921 
    +                                 (mkReflRedn role rhs)
    1922 
    +                             ; continueWith $ Right $
    1923 
    +                                 EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
    1924 
    +                                      , eq_lhs = lhs , eq_rhs = rhs }
    1925 
    +                             }
    1926 
    +                        | otherwise
    1927 
    +                        -> try_irred reason
    1928 
    +                  }
    1929 
    +         }
    1950 1930 
       -- Otherwise unification is off the table
    1951 1931 
       | otherwise
    1952 
    -  = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    1932 
    +  = finish_no_unify
    1953 1933
    1954 1934 
       where
    1955 
    -    -- Some problems prevent /unification/ but not /rewriting/
    1956 
    -    -- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
    1957 
    -    --    we can't unify (skolem-escape); but it /is/ canonical,
    1958 
    -    --    and hence we /can/ use it for rewriting
    1959 
    -    -- Concrete-ness:  alpha[conc] ~ b[sk]
    1960 
    -    --    We can use it to rewrite; we still have to solve the original
    1961 
    -    do_not_prevent_rewriting :: CheckTyEqResult
    1962 
    -    do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
    1963 
    -                               cteProblem cteConcrete
    1935 
    +    -- We can't unify, but this equality can go in the inert set
    1936 
    +    -- and be used to rewrite other constraints.
    1937 
    +    finish_no_unify =
    1938 
    +      canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    1939 
    +
    1940 
    +    -- We can't unify, and this equality should not be used to rewrite
    1941 
    +    -- other constraints (e.g. because it has an occurs check).
    1942 
    +    -- So add it to the inert Irreds.
    1943 
    +    try_irred reason =
    1944 
    +      tryIrredInstead reason ev eq_rel swapped lhs rhs
    1945 
    +
    1946 
    +    -- We can't unify as-is, and want to flip the equality around.
    1947 
    +    -- Example: alpha ~ F tys, flip it around to become the canonical
    1948 
    +    -- equality f tys ~ alpha.
    1949 
    +    swap_and_finish tv can_rhs =
    1950 
    +      swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
    1951 
    +
    1952 
    +    -- We can unify; go ahead and do so.
    1953 
    +    unify tv rhs_redn =
    1954 
    +
    1955 
    +      do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
    1956 
    +           -- the evidence, even if swapped=IsSwapped.   Suppose the original was
    1957 
    +           --     [W] co : Int ~ alpha
    1958 
    +           -- We unify alpha := Int, and set co := <Int>.  No need to
    1959 
    +           -- swap to   co = sym co'
    1960 
    +           --           co' = <Int>
    1961 
    +           new_ev <- if isReflCo (reductionCoercion rhs_redn)
    1962 
    +                     then return ev
    1963 
    +                     else rewriteEqEvidence emptyRewriterSet ev swapped
    1964 
    +                              (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
    1965 
    +
    1966 
    +         ; let tv_ty     = mkTyVarTy tv
    1967 
    +               final_rhs = reductionReducedType rhs_redn
    1968 
    +
    1969 
    +         ; traceTcS "Sneaky unification:" $
    1970 
    +           vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs,
    1971 
    +                 text "Coercion:" <+> pprEq tv_ty final_rhs,
    1972 
    +                 text "Left Kind is:" <+> ppr (typeKind tv_ty),
    1973 
    +                 text "Right Kind is:" <+> ppr (typeKind final_rhs) ]
    1974 
    +
    1975 
    +         -- Update the unification variable itself
    1976 
    +         ; unifyTyVar tv final_rhs
    1977 
    +
    1978 
    +         -- Provide Refl evidence for the constraint
    1979 
    +         -- Ignore 'swapped' because it's Refl!
    1980 
    +         ; setEvBindIfWanted new_ev EvCanonical $
    1981 
    +           evCoercion (mkNomReflCo final_rhs)
    1982 
    +
    1983 
    +         -- Kick out any constraints that can now be rewritten
    1984 
    +         ; kickOutAfterUnification [tv]
    1985 
    +
    1986 
    +         ; return (Stop new_ev (text "Solved by unification")) }
    1964 1987
    1965 1988 
     ---------------------------
    1966 1989 
     -- Unification is off the table
    ... ... @@ -1987,6 +2010,17 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    1987 2010 
     --              -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs
    1988 2011 
     --              | otherwise
    1989 2012
    2013 
    +              | reason `cterHasOnlyProblems` do_not_prevent_rewriting
    2014 
    +              -> do { let role = eqRelRole eq_rel
    2015 
    +                    ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
    2016 
    +                        (mkReflRedn role (canEqLHSType lhs))
    2017 
    +                        (mkReflRedn role rhs)
    2018 
    +                    ; continueWith $ Right $
    2019 
    +                        EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
    2020 
    +                             , eq_lhs = lhs , eq_rhs = rhs }
    2021 
    +                    }
    2022 
    +
    2023 
    +              | otherwise
    1990 2024 
                   -> tryIrredInstead reason ev eq_rel swapped lhs rhs
    1991 2025
    1992 2026 
                 PuOK _ rhs_redn
    ... ... @@ -2003,6 +2037,18 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
    2003 2037 
                                , eq_lhs = lhs
    2004 2038 
                                , eq_rhs = reductionReducedType rhs_redn } } }
    2005 2039
    2040 
    +-- | Some problems prevent /unification/ but not /rewriting/:
    2041 
    +--
    2042 
    +-- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
    2043 
    +--    we can't unify (skolem-escape); but it /is/ canonical,
    2044 
    +--    and hence we /can/ use it for rewriting
    2045 
    +--
    2046 
    +-- Concrete-ness:  alpha[conc] ~ b[sk]
    2047 
    +--    We can use it to rewrite; we still have to solve the original
    2048 
    +do_not_prevent_rewriting :: CheckTyEqResult
    2049 
    +do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
    2050 
    +                           cteProblem cteConcrete
    2051 
    +
    2006 2052 
     ----------------------
    2007 2053 
     swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
    2008 2054 
                   -> TcType -> CanEqLHS      -- ty ~ F tys
    ... ... @@ -2308,8 +2354,9 @@ and we turn this into
    2308 2354 
       [W] Arg alpha ~ cbv1
    2309 2355 
       [W] Res alpha ~ cbv2
    2310 2356
    2311 
    -where cbv1 and cbv2 are fresh TauTvs.  This is actually done by `break_wanted`
    2312 
    -in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`.
    2357 
    +where cbv1 and cbv2 are fresh TauTvs.  This is actually done within checkTyEqRhs,
    2358 
    +called within canEqCanLHSFinish_try_unification, which will use the BreakWanted
    2359 
    +FamAppBreaker.
    2313 2360
    2314 2361 
     Why TauTvs? See [Why TauTvs] below.
    2315 2362
    ... ... @@ -2318,7 +2365,7 @@ directly instead of calling wrapUnifierTcS. (Otherwise, we'd end up
    2318 2365 
     unifying cbv1 and cbv2 immediately, achieving nothing.)  Next, we
    2319 2366 
     unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
    2320 2367 
     unification happens immediately following a successful call to
    2321 
    -checkTouchableTyVarEq, in canEqCanLHSFinish_try_unification.
    2368 
    +checkTyEqRhs, in canEqCanLHSFinish_try_unification.
    2322 2369
    2323 2370 
     Now, we're here (including further context from our original example,
    2324 2371 
     from the top of the Note):

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -122,7 +122,7 @@ module GHC.Tc.Solver.Monad (
    122 122 
         pprEq,
    123 123
    124 124 
         -- Enforcing invariants for type equalities
    125 
    -    checkTypeEq, checkTouchableTyVarEq
    125 
    +    checkTypeEq
    126 126 
     ) where
    127 127
    128 128 
     import GHC.Prelude
    ... ... @@ -2169,129 +2169,36 @@ wrapUnifierX ev role do_unifications
    2169 2169 
     ************************************************************************
    2170 2170 
     -}
    2171 2171
    2172 
    -checkTouchableTyVarEq
    2173 
    -   :: CtEvidence
    2174 
    -   -> TcTyVar    -- A touchable meta-tyvar
    2175 
    -   -> TcType     -- The RHS
    2176 
    -   -> TcS (PuResult () Reduction)
    2177 
    --- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS
    2178 
    --- If checkTouchableTyVarEq tv ty = PuOK cts redn
    2179 
    ---   then we can unify
    2180 
    ---       tv := ty |> redn
    2181 
    ---   with extra wanteds 'cts'
    2182 
    --- If it returns (PuFail reason) we can't unify, and the reason explains why.
    2183 
    -checkTouchableTyVarEq ev lhs_tv rhs
    2184 
    -  | simpleUnifyCheck UC_Solver lhs_tv rhs   -- An (optional) short-cut
    2185 
    -  = do { traceTcS "checkTouchableTyVarEq: simple-check wins" (ppr lhs_tv $$ ppr rhs)
    2186 
    -       ; return (pure (mkReflRedn Nominal rhs)) }
    2187 
    -
    2188 
    -  | otherwise
    2189 
    -  = do { traceTcS "checkTouchableTyVarEq {" (ppr lhs_tv $$ ppr rhs)
    2190 
    -       ; check_result <- wrapTcS (check_rhs rhs)
    2191 
    -       ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
    2192 
    -       ; case check_result of
    2193 
    -            PuFail reason -> return (PuFail reason)
    2194 
    -            PuOK cts redn -> do { emitWork cts
    2195 
    -                                ; return (pure redn) } }
    2196 
    -
    2197 
    -  where
    2198 
    -    (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of
    2199 
    -       MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl)
    2200 
    -       _ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
    2201 
    -            -- lhs_tv should be a meta-tyvar
    2202 
    -
    2203 
    -    is_concrete_lhs_tv = isConcreteInfo lhs_tv_info
    2204 
    -
    2205 
    -    check_rhs rhs
    2206 
    -       -- Crucial special case for  alpha ~ F tys
    2207 
    -       -- We don't want to flatten that (F tys)!
    2208 
    -       | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs
    2209 
    -       = if is_concrete_lhs_tv
    2210 
    -         then failCheckWith (cteProblem cteConcrete)
    2211 
    -         else recurseIntoTyConApp arg_flags tc tys
    2212 
    -       | otherwise
    2213 
    -       = checkTyEqRhs flags rhs
    2214 
    -
    2215 
    -    flags = TEF { tef_foralls  = False -- isRuntimeUnkSkol lhs_tv
    2216 
    -                , tef_fam_app  = mkTEFA_Break ev NomEq break_wanted
    2217 
    -                , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl (LC_Promote False)
    2218 
    -                , tef_lhs      = TyVarLHS lhs_tv
    2219 
    -                , tef_occurs   = cteInsolubleOccurs }
    2220 
    -
    2221 
    -    arg_flags = famAppArgFlags flags
    2222 
    -
    2223 
    -    break_wanted :: FamAppBreaker Ct
    2224 
    -    break_wanted fam_app
    2225 
    -      -- Occurs check or skolem escape; so flatten
    2226 
    -      = do { let fam_app_kind = typeKind fam_app
    2227 
    -           ; reason <- checkPromoteFreeVars cteInsolubleOccurs
    2228 
    -                            lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind)
    2229 
    -           ; if not (cterHasNoProblem reason)  -- Failed to promote free vars
    2230 
    -             then failCheckWith reason
    2231 
    -             else
    2232 
    -        do { new_tv_ty <-
    2233 
    -              case lhs_tv_info of
    2234 
    -                ConcreteTv conc_info ->
    2235 
    -                  -- Make a concrete tyvar if lhs_tv is concrete
    2236 
    -                  -- e.g.  alpha[2,conc] ~ Maybe (F beta[4])
    2237 
    -                  --       We want to flatten to
    2238 
    -                  --       alpha[2,conc] ~ Maybe gamma[2,conc]
    2239 
    -                  --       gamma[2,conc] ~ F beta[4]
    2240 
    -                  TcM.newConcreteTyVarTyAtLevel conc_info lhs_tv_lvl fam_app_kind
    2241 
    -                _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind
    2242 
    -
    2243 
    -           ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
    2244 
    -           ; hole <- TcM.newVanillaCoercionHole pty
    2245 
    -           ; let new_ev = CtWanted { ctev_pred      = pty
    2246 
    -                                   , ctev_dest      = HoleDest hole
    2247 
    -                                   , ctev_loc       = cb_loc
    2248 
    -                                   , ctev_rewriters = ctEvRewriters ev }
    2249 
    -           ; return (PuOK (singleCt (mkNonCanonical new_ev))
    2250 
    -                          (mkReduction (HoleCo hole) new_tv_ty)) } }
    2251 
    -
    2252 
    -    -- See Detail (7) of the Note
    2253 
    -    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
    2254 
    -
    2255 
    -------------------------
    2256 2172 
     checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
    2257 2173 
                 -> TcS (PuResult () Reduction)
    2258 2174 
     -- Used for general CanEqLHSs, ones that do
    2259 2175 
     -- not have a touchable type variable on the LHS (i.e. not unifying)
    2260 
    -checkTypeEq ev eq_rel lhs rhs
    2261 
    -  | isGiven ev
    2262 
    -  = do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
    2263 
    -                                        , text "rhs:" <+> ppr rhs ])
    2264 
    -       ; check_result <- wrapTcS (check_given_rhs rhs)
    2265 
    -       ; traceTcS "checkTypeEq }" (ppr check_result)
    2266 
    -       ; case check_result of
    2267 
    -            PuFail reason -> return (PuFail reason)
    2268 
    -            PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
    2269 
    -                                ; emitWork new_givens
    2270 
    -                                ; updInertSet (addCycleBreakerBindings prs)
    2271 
    -                                ; return (pure redn) } }
    2272 
    -
    2273 
    -  | otherwise  -- Wanted
    2274 
    -  = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
    2275 
    -       ; case check_result of
    2276 
    -            PuFail reason -> return (PuFail reason)
    2277 
    -            PuOK cts redn -> do { emitWork cts
    2278 
    -                                ; return (pure redn) } }
    2176 
    +checkTypeEq ev eq_rel lhs rhs =
    2177 
    +  case ev of
    2178 
    +    CtGiven {} ->
    2179 
    +      do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
    2180 
    +                                          , text "rhs:" <+> ppr rhs ])
    2181 
    +         ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
    2182 
    +         ; traceTcS "checkTypeEq }" (ppr check_result)
    2183 
    +         ; case check_result of
    2184 
    +              PuFail reason -> return (PuFail reason)
    2185 
    +              PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
    2186 
    +                                  ; emitWork new_givens
    2187 
    +                                  ; updInertSet (addCycleBreakerBindings prs)
    2188 
    +                                  ; return (pure redn) } }
    2189 
    +    CtWanted {} ->
    2190 
    +      do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
    2191 
    +         ; case check_result of
    2192 
    +              PuFail reason -> return (PuFail reason)
    2193 
    +              PuOK cts redn -> do { emitWork cts
    2194 
    +                                  ; return (pure redn) } }
    2279 2195 
       where
    2280 
    -    check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
    2281 
    -    check_given_rhs rhs
    2282 
    -       -- See Note [Special case for top-level of Given equality]
    2283 
    -       | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs
    2284 
    -       = recurseIntoTyConApp arg_flags tc tys
    2285 
    -       | otherwise
    2286 
    -       = checkTyEqRhs given_flags rhs
    2287 
    -
    2288 
    -    arg_flags = famAppArgFlags given_flags
    2289 2196
    2290 2197 
         given_flags :: TyEqFlags (TcTyVar,TcType)
    2291 2198 
         given_flags = TEF { tef_lhs      = lhs
    2292 2199 
                           , tef_foralls  = False
    2293 2200 
                           , tef_unifying = NotUnifying
    2294 
    -                      , tef_fam_app  = mkTEFA_Break ev eq_rel break_given
    2201 
    +                      , tef_fam_app  = mkTEFA_Break ev eq_rel BreakGiven
    2295 2202 
                           , tef_occurs   = occ_prob }
    2296 2203 
             -- TEFA_Break used for: [G] a ~ Maybe (F a)
    2297 2204 
             --                   or [W] F a ~ Maybe (F a)
    ... ... @@ -2308,13 +2215,6 @@ checkTypeEq ev eq_rel lhs rhs
    2308 2215 
                      NomEq  -> cteInsolubleOccurs
    2309 2216 
                      ReprEq -> cteSolubleOccurs
    2310 2217
    2311 
    -    break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
    2312 
    -    break_given fam_app
    2313 
    -      = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
    2314 
    -           ; return (PuOK (unitBag (new_tv, fam_app))
    2315 
    -                          (mkReflRedn Nominal (mkTyVarTy new_tv))) }
    2316 
    -                    -- Why reflexive? See Detail (4) of the Note
    2317 
    -
    2318 2218 
         ---------------------------
    2319 2219 
         mk_new_given :: (TcTyVar, TcType) -> TcS Ct
    2320 2220 
         mk_new_given (new_tv, fam_app)
    ... ... @@ -2327,20 +2227,6 @@ checkTypeEq ev eq_rel lhs rhs
    2327 2227 
         -- See Detail (7) of the Note
    2328 2228 
         cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
    2329 2229
    2330 
    -mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
    2331 
    -mkTEFA_Break ev eq_rel breaker
    2332 
    -  | NomEq <- eq_rel
    2333 
    -  , not cycle_breaker_origin
    2334 
    -  = TEFA_Break breaker
    2335 
    -  | otherwise
    2336 
    -  = TEFA_Recurse
    2337 
    -  where
    2338 
    -    -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles]
    2339 
    -    -- in GHC.Tc.Solver.Equality
    2340 
    -    cycle_breaker_origin = case ctLocOrigin (ctEvLoc ev) of
    2341 
    -                              CycleBreakerOrigin {} -> True
    2342 
    -                              _                     -> False
    2343 
    -
    2344 2230 
     -------------------------
    2345 2231 
     -- | Fill in CycleBreakerTvs with the variables they stand for.
    2346 2232 
     -- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
    ... ... @@ -2357,31 +2243,6 @@ restoreTyVarCycles is
    2357 2243 
     (a ~R# b a) is soluble if b later turns out to be Identity
    2358 2244 
     So we treat this as a "soluble occurs check".
    2359 2245
    2360 
    -Note [Special case for top-level of Given equality]
    2361 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2362 
    -We take care when examining
    2363 
    -    [G] F ty ~ G (...(F ty)...)
    2364 
    -where both sides are TyFamLHSs.  We don't want to flatten that RHS to
    2365 
    -    [G] F ty ~ cbv
    2366 
    -    [G] G (...(F ty)...) ~ cbv
    2367 
    -Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a
    2368 
    -canonical constraint
    2369 
    -    [G] G (...(F ty)...) ~ F ty
    2370 
    -That tents to rewrite a big type to smaller one. This happens in T15703,
    2371 
    -where we had:
    2372 
    -    [G] Pure g ~ From1 (To1 (Pure g))
    2373 
    -Making a loop breaker and rewriting left to right just makes much bigger
    2374 
    -types than swapping it over.
    2375 
    -
    2376 
    -(We might hope to have swapped it over before getting to checkTypeEq,
    2377 
    -but better safe than sorry.)
    2378 
    -
    2379 
    -NB: We never see a TyVarLHS here, such as
    2380 
    -    [G] a ~ F tys here
    2381 
    -because we'd have swapped it to
    2382 
    -   [G] F tys ~ a
    2383 
    -in canEqCanLHS2, before getting to checkTypeEq.
    2384 
    -
    2385 2246 
     Note [Don't cycle-break Wanteds when not unifying]
    2386 2247 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2387 2248 
     Consdier

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -257,10 +257,10 @@ We thus perform an occurs-check. There is, of course, some subtlety:
    257 257
    258 258 
     * For type variables, the occurs-check looks deeply including kinds of
    259 259 
       type variables. This is because a CEqCan over a meta-variable is
    260 
    -  also used to inform unification, in
    261 
    -  GHC.Tc.Solver.Monad.checkTouchableTyVarEq. If the LHS appears
    262 
    -  anywhere in the RHS, at all, unification will create an infinite
    263 
    -  structure which is bad.
    260 
    +  also used to inform unification, via `checkTyEqRhs`, called in
    261 
    +  `canEqCanLHSFinish_try_unification`.
    262 
    +  If the LHS appears anywhere in the RHS, at all, unification will create
    263 
    +  an infinite structure, which is bad.
    264 264
    265 265 
     * For type family applications, the occurs-check is shallow; it looks
    266 266 
       only in places where we might rewrite. (Specifically, it does not

  • compiler/GHC/Tc/Utils/Unify.hs
    1 
    +{-# LANGUAGE GADTs               #-}
    2 
    +{-# LANGUAGE DerivingStrategies  #-}
    3 
    +{-# LANGUAGE LambdaCase          #-}
    1 4 
     {-# LANGUAGE ScopedTypeVariables #-}
    2 5 
     {-# LANGUAGE TupleSections       #-}
    3 6 
     {-# LANGUAGE RecursiveDo         #-}
    ... ... @@ -25,7 +28,7 @@ module GHC.Tc.Utils.Unify (
    25 28 
       -- Various unifications
    26 29 
       unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
    27 30 
       unifyExprType, unifyTypeAndEmit, promoteTcType,
    28 
    -  swapOverTyVars, touchabilityAndShapeTest, checkTopShape, lhsPriority,
    31 
    +  swapOverTyVars, touchabilityTest, checkTopShape, lhsPriority,
    29 32 
       UnifyEnv(..), updUEnvLoc, setUEnvRole,
    30 33 
       uType,
    31 34
    ... ... @@ -39,11 +42,12 @@ module GHC.Tc.Utils.Unify (
    39 42 
       matchExpectedFunKind,
    40 43 
       matchActualFunTy, matchActualFunTys,
    41 44
    42 
    -  checkTyEqRhs, recurseIntoTyConApp,
    45 
    +  checkTyEqRhs, recurseIntoTyConApp, recurseIntoFamTyConApp,
    43 46 
       PuResult(..), failCheckWith, okCheckRefl, mapCheck,
    44 
    -  TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
    45 
    -  famAppArgFlags,  checkPromoteFreeVars,
    46 
    -  simpleUnifyCheck, UnifyCheckCaller(..),
    47 
    +  TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker(..),
    48 
    +  famAppArgFlags, checkPromoteFreeVars,
    49 
    +  notUnifying_TEFTask, unifyingLHSMetaTyVar_TEFTask, mkTEFA_Break,
    50 
    +  simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..),
    47 51
    48 52 
       fillInferResult,
    49 53 
       ) where
    ... ... @@ -60,7 +64,8 @@ import GHC.Tc.Utils.TcMType
    60 64 
     import GHC.Tc.Utils.TcType
    61 65 
     import GHC.Tc.Types.Evidence
    62 66 
     import GHC.Tc.Types.Constraint
    63 
    -import GHC.Tc.Types.CtLoc( CtLoc, mkKindEqLoc, adjustCtLoc )
    67 
    +import GHC.Tc.Types.CtLoc( CtLoc, mkKindEqLoc, adjustCtLoc
    68 
    +                         , ctLocOrigin, updateCtLocOrigin )
    64 69 
     import GHC.Tc.Types.Origin
    65 70 
     import GHC.Tc.Zonk.TcType
    66 71
    ... ... @@ -71,6 +76,7 @@ import GHC.Core.TyCo.Ppr( debugPprType {- pprTyVar -} )
    71 76 
     import GHC.Core.TyCon
    72 77 
     import GHC.Core.Coercion
    73 78 
     import GHC.Core.Multiplicity
    79 
    +import GHC.Core.Predicate ( EqRel(..) )
    74 80 
     import GHC.Core.Reduction
    75 81
    76 82 
     import qualified GHC.LanguageExtensions as LangExt
    ... ... @@ -96,6 +102,7 @@ import GHC.Data.FastString( fsLit )
    96 102 
     import Control.Monad
    97 103 
     import Data.Monoid as DM ( Any(..) )
    98 104 
     import qualified Data.Semigroup as S ( (<>) )
    105 
    +import Data.Traversable ( for )
    99 106
    100 107 
     {- *********************************************************************
    101 108 
     *                                                                      *
    ... ... @@ -2477,10 +2484,9 @@ uUnfilledVar2 :: UnifyEnv -- Precondition: u_role==Nominal
    2477 2484 
     uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
    2478 2485 
       = do { cur_lvl <- getTcLevel
    2479 2486 
                -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
    2480 
    -           -- Here we don't know about given equalities here; so we treat
    2487 
    +           -- Here we don't know about given equalities; so we treat
    2481 2488 
                -- /any/ level outside this one as untouchable.  Hence cur_lvl.
    2482 
    -       ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2
    2483 
    -                 && simpleUnifyCheck UC_OnTheFly tv1 ty2)
    2489 
    +       ; if simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2 /= SUC_CanUnify
    2484 2490 
              then not_ok_so_defer cur_lvl
    2485 2491 
              else
    2486 2492 
         do { def_eqs <- readTcRef def_eq_ref  -- Capture current state of def_eqs
    ... ... @@ -2525,8 +2531,8 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
    2525 2531 
           do { traceTc "uUnfilledVar2 not ok" $
    2526 2532 
                  vcat [ text "tv1:" <+> ppr tv1
    2527 2533 
                       , text "ty2:" <+> ppr ty2
    2528 
    -                  , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly tv1 ty2)
    2529 
    -                  , text "touchability:" <+> ppr (touchabilityAndShapeTest cur_lvl tv1 ty2)]
    2534 
    +                  , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2)
    2535 
    +                  ]
    2530 2536 
                    -- Occurs check or an untouchable: just defer
    2531 2537 
                    -- NB: occurs check isn't necessarily fatal:
    2532 2538 
                    --     eg tv1 occurred in type family parameter
    ... ... @@ -2585,9 +2591,8 @@ lhsPriority tv
    2585 2591 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2586 2592 
     Question: given a homogeneous equality (alpha ~# ty), when is it OK to
    2587 2593 
     unify alpha := ty?
    2588 
    -
    2589 
    -This note only applied to /homogeneous/ equalities, in which both
    2590 
    -sides have the same kind.
    2594 
    +(This note only applies to /homogeneous/ equalities, in which both
    2595 
    +sides have the same kind.)
    2591 2596
    2592 2597 
     There are five reasons not to unify:
    2593 2598
    ... ... @@ -2681,7 +2686,7 @@ Needless to say, all there are wrinkles:
    2681 2686
    2682 2687 
       * In the constraint solver, we track where Given equalities occur
    2683 2688 
         and use that to guard unification in
    2684 
    -    GHC.Tc.Utils.Unify.touchabilityAndShapeTest. More details in
    2689 
    +    GHC.Tc.Utils.Unify.touchabilityTest. More details in
    2685 2690 
         Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
    2686 2691
    2687 2692 
         Historical note: in the olden days (pre 2021) the constraint solver
    ... ... @@ -2922,12 +2927,34 @@ data UnifyCheckCaller
    2922 2927 
       = UC_OnTheFly   -- Called from the on-the-fly unifier
    2923 2928 
       | UC_QuickLook  -- Called from Quick Look
    2924 2929 
       | UC_Solver     -- Called from constraint solver
    2925 
    -  | UC_Defaulting -- Called when doing top-level defaulting
    2926 2930
    2927 
    -simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
    2928 
    --- simpleUnifyCheck does a fast check: True <=> unification is OK
    2929 
    --- If it says 'False' then unification might still be OK, but
    2930 
    --- it'll take more work to do -- use the full checkTypeEq
    2931 
    +-- | The result type of 'simpleUnifyCheck'.
    2932 
    +data SimpleUnifyResult
    2933 
    +  -- | Definitely cannot unify (untouchable variable or incompatible top-shape)
    2934 
    +  = SUC_CannotUnify
    2935 
    +  -- | The variable is touchable and the top-shape test passed, but
    2936 
    +  -- it may or may not be OK to unify
    2937 
    +  | SUC_NotSure
    2938 
    +  -- | Definitely OK to unify
    2939 
    +  | SUC_CanUnify
    2940 
    +  deriving stock (Eq, Ord, Show)
    2941 
    +instance Semigroup SimpleUnifyResult where
    2942 
    +  no@SUC_CannotUnify <> _ = no
    2943 
    +  SUC_CanUnify <> r = r
    2944 
    +  _ <> no@SUC_CannotUnify = no
    2945 
    +  r <> SUC_CanUnify = r
    2946 
    +  ns@SUC_NotSure <> SUC_NotSure = ns
    2947 
    +
    2948 
    +instance Outputable SimpleUnifyResult where
    2949 
    +  ppr = \case
    2950 
    +    SUC_CannotUnify -> text "SUC_CannotUnify"
    2951 
    +    SUC_NotSure     -> text "SUC_NotSure"
    2952 
    +    SUC_CanUnify    -> text "SUC_CanUnify"
    2953 
    +
    2954 
    +simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult
    2955 
    +-- ^ A fast check for unification. May return "not sure", in which case
    2956 
    +-- unification might still be OK, but it'll take more work to do
    2957 
    +-- (use the full 'checkTypeEq').
    2931 2958 
     --
    2932 2959 
     -- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
    2933 2960 
     -- * Rejects foralls unless
    ... ... @@ -2938,9 +2965,17 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
    2938 2965 
     -- * Does a level-check for type variables, to avoid skolem escape
    2939 2966 
     --
    2940 2967 
     -- This function is pretty heavily used, so it's optimised not to allocate
    2941 
    -simpleUnifyCheck caller lhs_tv rhs
    2942 
    -  = go rhs
    2968 
    +simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
    2969 
    +  | not $ touchabilityTest given_eq_lvl lhs_tv
    2970 
    +  = SUC_CannotUnify
    2971 
    +  | not $ checkTopShape lhs_info rhs
    2972 
    +  = SUC_CannotUnify
    2973 
    +  | rhs_is_ok rhs
    2974 
    +  = SUC_CanUnify
    2975 
    +  | otherwise
    2976 
    +  = SUC_NotSure
    2943 2977 
       where
    2978 
    +    lhs_info = metaTyVarInfo lhs_tv
    2944 2979
    2945 2980 
         !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv
    2946 2981
    ... ... @@ -2960,33 +2995,32 @@ simpleUnifyCheck caller lhs_tv rhs
    2960 2995 
                    UC_Solver     -> True
    2961 2996 
                    UC_QuickLook  -> True
    2962 2997 
                    UC_OnTheFly   -> False
    2963 
    -               UC_Defaulting -> True
    2964 2998
    2965 
    -    go (TyVarTy tv)
    2999 
    +    rhs_is_ok (TyVarTy tv)
    2966 3000 
           | lhs_tv == tv                                    = False
    2967 3001 
           | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False
    2968 3002 
           | lhs_tv_is_concrete, not (isConcreteTyVar tv)    = False
    2969 3003 
           | occ_in_ty $! (tyVarKind tv)                     = False
    2970 3004 
           | otherwise                                       = True
    2971 3005
    2972 
    -    go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
    3006 
    +    rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
    2973 3007 
           | not forall_ok, isInvisibleFunArg af = False
    2974 
    -      | otherwise                           = go w && go a && go r
    3008 
    +      | otherwise                           = rhs_is_ok w && rhs_is_ok a && rhs_is_ok r
    2975 3009
    2976 
    -    go (TyConApp tc tys)
    3010 
    +    rhs_is_ok (TyConApp tc tys)
    2977 3011 
           | lhs_tv_is_concrete, not (isConcreteTyCon tc) = False
    2978 3012 
           | not forall_ok, not (isTauTyCon tc)           = False
    2979 3013 
           | not fam_ok,    not (isFamFreeTyCon tc)       = False
    2980 
    -      | otherwise                                    = all go tys
    3014 
    +      | otherwise                                    = all rhs_is_ok tys
    2981 3015
    2982 
    -    go (ForAllTy (Bndr tv _) ty)
    2983 
    -      | forall_ok = go (tyVarKind tv) && (tv == lhs_tv || go ty)
    3016 
    +    rhs_is_ok (ForAllTy (Bndr tv _) ty)
    3017 
    +      | forall_ok = rhs_is_ok (tyVarKind tv) && (tv == lhs_tv || rhs_is_ok ty)
    2984 3018 
           | otherwise = False
    2985 3019
    2986 
    -    go (AppTy t1 t2)    = go t1 && go t2
    2987 
    -    go (CastTy ty co)   = not (occ_in_co co) && go ty
    2988 
    -    go (CoercionTy co)  = not (occ_in_co co)
    2989 
    -    go (LitTy {})       = True
    3020 
    +    rhs_is_ok (AppTy t1 t2)    = rhs_is_ok t1 && rhs_is_ok t2
    3021 
    +    rhs_is_ok (CastTy ty co)   = not (occ_in_co co) && rhs_is_ok ty
    3022 
    +    rhs_is_ok (CoercionTy co)  = not (occ_in_co co)
    3023 
    +    rhs_is_ok (LitTy {})       = True
    2990 3024
    2991 3025
    2992 3026 
     mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool)
    ... ... @@ -3073,10 +3107,7 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`.
    3073 3107
    3074 3108 
     data PuResult a b = PuFail CheckTyEqResult
    3075 3109 
                       | PuOK (Bag a) b
    3076 
    -
    3077 
    -instance Functor (PuResult a) where
    3078 
    -  fmap _ (PuFail prob) = PuFail prob
    3079 
    -  fmap f (PuOK cts x)  = PuOK cts (f x)
    3110 
    +                  deriving stock (Functor, Foldable, Traversable)
    3080 3111
    3081 3112 
     instance Applicative (PuResult a) where
    3082 3113 
       pure x = PuOK emptyBag x
    ... ... @@ -3192,15 +3223,147 @@ famAppArgFlags flags@(TEF { tef_unifying = unifying })
    3192 3223 
                   | not deeply = Unifying info lvl LC_Check
    3193 3224 
         zap_promotion unifying = unifying
    3194 3225
    3195 
    -type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)
    3196 
    -     -- Given a family-application ty, return a Reduction :: ty ~ cvb
    3197 
    -     -- where 'cbv' is a fresh loop-breaker tyvar (for Given), or
    3198 
    -     -- just a fresh TauTv (for Wanted)
    3226 
    +-- | How to break a family-application cycle when checking a type equality.
    3227 
    +-- Given a family-application @fam_app@, return a @'Reduction' :: fam_app ~ cbv@
    3228 
    +-- where @cbv@ is a fresh cycle-breaker tyvar (for Given), or
    3229 
    +-- a fresh 'TauTv' (for Wanted).
    3230 
    +data FamAppBreaker a where
    3231 
    +  BreakGiven  :: FamAppBreaker (TcTyVar, TcType)
    3232 
    +  BreakWanted :: CtEvidence -> TcTyVar -> FamAppBreaker Ct
    3233 
    +
    3234 
    +-- | Dispatch on a 'FamAppBreaker' to break a family-application cycle.
    3235 
    +-- See Note [Type equality cycles] in GHC.Tc.Solver.Equality.
    3236 
    +famAppBreaker :: FamAppBreaker a -> TcType -> TcM (PuResult a Reduction)
    3237 
    +famAppBreaker BreakGiven fam_app
    3238 
    +  -- Why reflexive? See Detail (4) of Note [Type equality cycles] in GHC.Tc.Solver.Equality
    3239 
    +  = do { new_tv <- newCycleBreakerTyVar (typeKind fam_app)
    3240 
    +       ; return (PuOK (unitBag (new_tv, fam_app))
    3241 
    +                      (mkReflRedn Nominal (mkTyVarTy new_tv))) }
    3242 
    +famAppBreaker (BreakWanted ev lhs_tv) fam_app
    3243 
    +  -- Occurs check or skolem escape; so flatten.
    3244 
    +  = do { let fam_app_kind = typeKind fam_app
    3245 
    +       ; reason <- checkPromoteFreeVars cteInsolubleOccurs
    3246 
    +                     lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind)
    3247 
    +       ; if not (cterHasNoProblem reason)  -- Failed to promote free vars
    3248 
    +         then return $ PuFail reason
    3249 
    +         else
    3250 
    +    do { new_tv_ty <-
    3251 
    +          case lhs_tv_info of
    3252 
    +            ConcreteTv conc_info ->
    3253 
    +              -- Make a concrete tyvar if lhs_tv is concrete
    3254 
    +              -- e.g.  alpha[2,conc] ~ Maybe (F beta[4])
    3255 
    +              --       We want to flatten to
    3256 
    +              --       alpha[2,conc] ~ Maybe gamma[2,conc]
    3257 
    +              --       gamma[2,conc] ~ F beta[4]
    3258 
    +              newConcreteTyVarTyAtLevel conc_info lhs_tv_lvl fam_app_kind
    3259 
    +            _ -> newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind
    3260 
    +       ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
    3261 
    +       ; hole <- newVanillaCoercionHole pty
    3262 
    +       ; let new_ev = CtWanted { ctev_pred      = pty
    3263 
    +                               , ctev_dest      = HoleDest hole
    3264 
    +                               , ctev_loc       = cb_loc
    3265 
    +                               , ctev_rewriters = ctEvRewriters ev }
    3266 
    +       ; return (PuOK (singleCt (mkNonCanonical new_ev))
    3267 
    +                      (mkReduction (HoleCo hole) new_tv_ty)) } }
    3268 
    +  where
    3269 
    +    (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of
    3270 
    +       MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl)
    3271 
    +       _ -> pprPanic "famAppBreaker BreakWanted: lhs_tv is not a meta-tyvar" (ppr lhs_tv)
    3272 
    +    -- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Equality
    3273 
    +    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
    3274 
    +
    3275 
    +instance Outputable (FamAppBreaker a) where
    3276 
    +  ppr BreakGiven          = text "BreakGiven"
    3277 
    +  ppr (BreakWanted ev tv) = parens $ text "BreakWanted" <+> ppr ev <+> ppr tv
    3278 
    +
    3279 
    +tefConcrete :: TyEqFlags a -> Bool
    3280 
    +tefConcrete (TEF { tef_unifying = Unifying info _ _ }) = isConcreteInfo info
    3281 
    +tefConcrete (TEF { tef_unifying = NotUnifying })       = False
    3282 
    +
    3283 
    +mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
    3284 
    +mkTEFA_Break ev eq_rel breaker
    3285 
    +  | NomEq <- eq_rel
    3286 
    +  , not cycle_breaker_origin
    3287 
    +  = TEFA_Break breaker
    3288 
    +  | otherwise
    3289 
    +  = TEFA_Recurse
    3290 
    +  where
    3291 
    +    -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles]
    3292 
    +    -- in GHC.Tc.Solver.Equality
    3293 
    +    cycle_breaker_origin = case ctLocOrigin (ctEvLoc ev) of
    3294 
    +                              CycleBreakerOrigin {} -> True
    3295 
    +                              _                     -> False
    3296 
    +
    3297 
    +notUnifying_TEFTask :: CheckTyEqProblem -> CanEqLHS -> TyEqFlags a
    3298 
    +-- Used for the non-unifying cases (checkTypeEq in Solver.Monad)
    3299 
    +notUnifying_TEFTask occ_prob lhs
    3300 
    +  = TEF { tef_foralls  = False
    3301 
    +        , tef_lhs      = lhs
    3302 
    +        , tef_unifying = NotUnifying
    3303 
    +        , tef_fam_app  = TEFA_Recurse
    3304 
    +        , tef_occurs   = occ_prob }
    3305 
    +
    3306 
    +unifyingLHSMetaTyVar_TEFTask :: CtEvidence -> TcTyVar -> TyEqFlags Ct
    3307 
    +-- Used for the unifying case (canEqCanLHSFinish_try_unification in Solver.Equality)
    3308 
    +unifyingLHSMetaTyVar_TEFTask ev lhs_tv
    3309 
    +  = TEF { tef_foralls  = False
    3310 
    +        , tef_fam_app  = mkTEFA_Break ev NomEq (BreakWanted ev lhs_tv)
    3311 
    +        , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl (LC_Promote False)
    3312 
    +        , tef_lhs      = TyVarLHS lhs_tv
    3313 
    +        , tef_occurs   = cteInsolubleOccurs }
    3314 
    +  where
    3315 
    +    (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of
    3316 
    +      MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info, lvl)
    3317 
    +      _ -> pprPanic "unifyingLHSMetaTyVar_TEFTask: not a meta-tyvar" (ppr lhs_tv)
    3199 3318
    3200 3319 
     checkTyEqRhs :: forall a. TyEqFlags a
    3201 3320 
                            -> TcType           -- Already zonked
    3202 3321 
                            -> TcM (PuResult a Reduction)
    3203 
    -checkTyEqRhs flags ty
    3322 
    +-- Crucial special case for a top-level equality of the form 'alpha ~ F tys'.
    3323 
    +-- We don't want to flatten that (F tys), as this gets us right back to where
    3324 
    +-- we started!
    3325 
    +-- See also Note [Special case for top-level of Given equality]
    3326 
    +checkTyEqRhs flags rhs
    3327 
    +  | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs
    3328 
    +  , not $ tefConcrete flags
    3329 
    +  = recurseIntoFamTyConApp flags tc tys
    3330 
    +  | otherwise
    3331 
    +  = check_ty_eq_rhs flags rhs
    3332 
    +
    3333 
    +{- Note [Special case for top-level of Given equality]
    3334 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    3335 
    +We take care when examining
    3336 
    +    [G] F ty ~ G (...(F ty)...)
    3337 
    +where both sides are TyFamLHSs.  We don't want to flatten that RHS to
    3338 
    +    [G] F ty ~ cbv
    3339 
    +    [G] G (...(F ty)...) ~ cbv
    3340 
    +Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a
    3341 
    +canonical constraint
    3342 
    +    [G] G (...(F ty)...) ~ F ty
    3343 
    +That tends to rewrite a big type to smaller one. This happens in T15703,
    3344 
    +where we had:
    3345 
    +    [G] Pure g ~ From1 (To1 (Pure g))
    3346 
    +Making a loop breaker and rewriting left to right just makes much bigger
    3347 
    +types than swapping it over.
    3348 
    +
    3349 
    +(We might hope to have swapped it over before getting to checkTypeEq,
    3350 
    +but better safe than sorry.)
    3351 
    +
    3352 
    +NB: We never see a TyVarLHS here, such as
    3353 
    +    [G] a ~ F tys here
    3354 
    +because we'd have swapped it to
    3355 
    +   [G] F tys ~ a
    3356 
    +in canEqCanLHS2, before getting to checkTypeEq.
    3357 
    +-}
    3358 
    +
    3359 
    +recurseIntoFamTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
    3360 
    +recurseIntoFamTyConApp flags tc tys
    3361 
    +  = recurseIntoTyConApp (famAppArgFlags flags) tc tys
    3362 
    +
    3363 
    +check_ty_eq_rhs :: forall a. TyEqFlags a
    3364 
    +                           -> TcType           -- Already zonked
    3365 
    +                           -> TcM (PuResult a Reduction)
    3366 
    +check_ty_eq_rhs flags ty
    3204 3367 
       = case ty of
    3205 3368 
           LitTy {}        -> okCheckRefl ty
    3206 3369 
           TyConApp tc tys -> checkTyConApp flags ty tc tys
    ... ... @@ -3214,26 +3377,24 @@ checkTyEqRhs flags ty
    3214 3377 
            , not (tef_foralls flags)
    3215 3378 
            -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F)
    3216 3379 
            | otherwise
    3217 
    -       -> do { w_res <- checkTyEqRhs flags w
    3218 
    -             ; a_res <- checkTyEqRhs flags a
    3219 
    -             ; r_res <- checkTyEqRhs flags r
    3380 
    +       -> do { w_res <- check_ty_eq_rhs flags w
    3381 
    +             ; a_res <- check_ty_eq_rhs flags a
    3382 
    +             ; r_res <- check_ty_eq_rhs flags r
    3220 3383 
                  ; return (mkFunRedn Nominal af <$> w_res <*> a_res <*> r_res) }
    3221 3384
    3222 
    -      AppTy fun arg -> do { fun_res <- checkTyEqRhs flags fun
    3223 
    -                          ; arg_res <- checkTyEqRhs flags arg
    3385 
    +      AppTy fun arg -> do { fun_res <- check_ty_eq_rhs flags fun
    3386 
    +                          ; arg_res <- check_ty_eq_rhs flags arg
    3224 3387 
                               ; return (mkAppRedn <$> fun_res <*> arg_res) }
    3225 3388
    3226 
    -      CastTy ty co  -> do { ty_res <- checkTyEqRhs flags ty
    3389 
    +      CastTy ty co  -> do { ty_res <- check_ty_eq_rhs flags ty
    3227 3390 
                               ; co_res <- checkCo flags co
    3228 3391 
                               ; return (mkCastRedn1 Nominal ty <$> co_res <*> ty_res) }
    3229 3392
    3230 3393 
           CoercionTy co -> do { co_res <- checkCo flags co
    3231 3394 
                               ; return (mkReflCoRedn Nominal <$> co_res) }
    3232 3395
    3233 
    -      ForAllTy {}
    3234 
    -         | tef_foralls flags -> okCheckRefl ty
    3235 
    -         | otherwise         -> failCheckWith impredicativeProblem  -- Not allowed (TyEq:F)
    3236 
    -
    3396 
    +      ForAllTy {}   -> return $ PuFail impredicativeProblem -- Not allowed (TyEq:F)
    3397 
    +{-# INLINEABLE check_ty_eq_rhs #-}
    3237 3398
    3238 3399 
     -------------------
    3239 3400 
     checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
    ... ... @@ -3388,15 +3549,14 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
    3388 3549 
         else do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
    3389 3550 
                       fun_app                = mkTyConApp tc fun_args
    3390 3551 
                 ; fun_res   <- checkFamApp flags fun_app tc fun_args
    3391 
    -            ; extra_res <- mapCheck (checkTyEqRhs flags) extra_args
    3392 
    -            ; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res)
    3552 
    +            ; extra_res <- mapCheck (check_ty_eq_rhs flags) extra_args
    3393 3553 
                 ; return (mkAppRedns <$> fun_res <*> extra_res) }
    3394 3554
    3395 3555 
       | Just ty' <- rewriterView tc_app
    3396 3556 
            -- e.g. S a  where  type S a = F [a]
    3397 3557 
            --             or   type S a = Int
    3398 3558 
            -- See Note [Forgetful synonyms in checkTyConApp]
    3399 
    -  = checkTyEqRhs flags ty'
    3559 
    +  = check_ty_eq_rhs flags ty'
    3400 3560
    3401 3561 
       | not (isTauTyCon tc || foralls_ok)
    3402 3562 
       = failCheckWith impredicativeProblem
    ... ... @@ -3411,7 +3571,7 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
    3411 3571
    3412 3572 
     recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
    3413 3573 
     recurseIntoTyConApp flags tc tys
    3414 
    -  = do { tys_res <- mapCheck (checkTyEqRhs flags) tys
    3574 
    +  = do { tys_res <- mapCheck (check_ty_eq_rhs flags) tys
    3415 3575 
            ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
    3416 3576
    3417 3577 
     -------------------
    ... ... @@ -3430,16 +3590,16 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
    3430 3590 
             , tcEqTyConApps lhs_tc lhs_tys tc tys
    3431 3591 
             -> case fam_app_flag of
    3432 3592 
                  TEFA_Recurse       -> failCheckWith (cteProblem occ_prob)
    3433 
    -             TEFA_Break breaker -> breaker fam_app
    3593 
    +             TEFA_Break breaker -> famAppBreaker breaker fam_app
    3434 3594
    3435 3595 
           _ | Unifying lhs_info _ _ <- unifying
    3436 3596 
             , isConcreteInfo lhs_info
    3437 3597 
             -> case fam_app_flag of
    3438 3598 
                  TEFA_Recurse       -> failCheckWith (cteProblem cteConcrete)
    3439 
    -             TEFA_Break breaker -> breaker fam_app
    3599 
    +             TEFA_Break breaker -> famAppBreaker breaker fam_app
    3440 3600
    3441 3601 
           TEFA_Recurse
    3442 
    -        -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
    3602 
    +        -> do { tys_res <- mapCheck (check_ty_eq_rhs arg_flags) tys
    3443 3603 
                   ; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags)
    3444 3604 
                   ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
    3445 3605
    ... ... @@ -3448,16 +3608,16 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
    3448 3608 
           --       alpha[2] ~ Maybe (F beta[4])    Level-check problem: break
    3449 3609 
           -- NB: in the latter case, don't promote beta[4]; hence arg_flags!
    3450 3610 
           TEFA_Break breaker
    3451 
    -        -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
    3611 
    +        -> do { tys_res <- mapCheck (check_ty_eq_rhs arg_flags) tys
    3452 3612 
                   ; case tys_res of
    3453 3613 
                       PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns))
    3454 
    -                  PuFail {}      -> breaker fam_app }
    3614 
    +                  PuFail {}      -> famAppBreaker breaker fam_app }
    3455 3615 
       where
    3456 3616 
         arg_flags = famAppArgFlags flags
    3457 3617
    3458 3618 
     -------------------
    3459 3619 
     checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
    3460 
    -checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv
    3620 
    +checkTyVar flags@(TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv
    3461 3621 
       = case lhs of
    3462 3622 
           TyFamLHS {}     -> success   -- Nothing to do if the LHS is a type-family
    3463 3623 
           TyVarLHS lhs_tv -> check_tv unifying lhs_tv
    ... ... @@ -3491,7 +3651,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
    3491 3651 
           | isConcreteInfo lhs_tv_info
    3492 3652 
           , not (isConcreteTyVar occ_tv)
    3493 3653 
           = if can_make_concrete occ_tv
    3494 
    -        then promote lhs_tv lhs_tv_info lhs_tv_lvl
    3654 
    +        then promote lhs_tv_info lhs_tv_lvl
    3495 3655 
             else failCheckWith (cteProblem cteConcrete)
    3496 3656
    3497 3657 
           | lvl_occ `strictlyDeeperThan` lhs_tv_lvl
    ... ... @@ -3500,7 +3660,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
    3500 3660 
                LC_Check   -> failCheckWith (cteProblem cteSkolemEscape)
    3501 3661 
                LC_Promote {}
    3502 3662 
                  | isSkolemTyVar occ_tv  -> failCheckWith (cteProblem cteSkolemEscape)
    3503 
    -             | otherwise             -> promote lhs_tv lhs_tv_info lhs_tv_lvl
    3663 
    +             | otherwise             -> promote lhs_tv_info lhs_tv_lvl
    3504 3664
    3505 3665 
           | otherwise
    3506 3666 
           = simple_occurs_check lhs_tv
    ... ... @@ -3525,7 +3685,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
    3525 3685
    3526 3686 
         ---------------------
    3527 3687 
         -- occ_tv is definitely a MetaTyVar
    3528 
    -    promote lhs_tv lhs_tv_info lhs_tv_lvl
    3688 
    +    promote lhs_tv_info lhs_tv_lvl
    3529 3689 
           | MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- tcTyVarDetails occ_tv
    3530 3690 
           = do { let new_info | isConcreteInfo lhs_tv_info = lhs_tv_info
    3531 3691 
                               | otherwise                  = info_occ
    ... ... @@ -3534,12 +3694,23 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
    3534 3694 
                                -- c[tau,2]  ~ p[tau,3]: want to clone p:=p'[tau,2]
    3535 3695
    3536 3696 
                -- Check the kind of occ_tv
    3537 
    -           ; reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
    3538 
    -
    3539 
    -           ; if cterHasNoProblem reason  -- Successfully promoted
    3540 
    -             then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
    3541 
    -                     ; okCheckRefl new_tv_ty }
    3542 
    -             else failCheckWith reason }
    3697 
    +           --
    3698 
    +           -- This is important for several reasons:
    3699 
    +           --
    3700 
    +           --  1. To ensure there is no occurs check or skolem-escape
    3701 
    +           --     in the kind of occ_tv.
    3702 
    +           --  2. If the LHS is a concrete type variable and the RHS is an
    3703 
    +           --     unfilled meta-tyvar, we need to ensure that the kind of
    3704 
    +           --     'occ_tv' is concrete.   Test cases: T23051, T23176.
    3705 
    +           ; let occ_kind = tyVarKind occ_tv
    3706 
    +           ; kind_result <- check_ty_eq_rhs flags occ_kind
    3707 
    +           ; for kind_result $ \ kind_redn ->
    3708 
    +        do { let kind_co  = reductionCoercion kind_redn
    3709 
    +                 new_kind = reductionReducedType kind_redn
    3710 
    +                 occ_tv'  = setTyVarKind occ_tv new_kind
    3711 
    +           ; new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv'
    3712 
    +           ; return $ mkGReflLeftRedn Nominal new_tv_ty (mkSymCo kind_co)
    3713 
    +           } }
    3543 3714
    3544 3715 
           | otherwise = pprPanic "promote" (ppr occ_tv)
    3545 3716
    ... ... @@ -3591,16 +3762,15 @@ promote_meta_tyvar info dest_lvl occ_tv
    3591 3762
    3592 3763
    3593 3764 
     -------------------------
    3594 
    -touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
    3595 
    --- This is the key test for untouchability:
    3765 
    +touchabilityTest :: TcLevel -> TcTyVar -> Bool
    3766 
    +-- ^ This is the key test for untouchability:
    3596 3767 
     -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
    3597 3768 
     -- and Note [Solve by unification] in GHC.Tc.Solver.Equality
    3598 
    --- True <=> touchability and shape are OK
    3599 
    -touchabilityAndShapeTest given_eq_lvl tv rhs
    3600 
    -  | MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
    3601 
    -  , tv_lvl `deeperThanOrSame` given_eq_lvl
    3602 
    -  , checkTopShape info rhs
    3603 
    -  = True
    3769 
    +--
    3770 
    +-- @True@ <=> the variable is touchable
    3771 
    +touchabilityTest given_eq_lvl tv
    3772 
    +  | MetaTv { mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
    3773 
    +  = tv_lvl `deeperThanOrSame` given_eq_lvl
    3604 3774 
       | otherwise
    3605 3775 
       = False
    3606 3776

  • testsuite/tests/rep-poly/T19709b.stderr
    1 
    -
    2 1 
     T19709b.hs:11:15: error: [GHC-55287]
    3 2 
         • The argument ‘(error @Any "e2")’ of ‘levfun’
    4 3 
           does not have a fixed runtime representation.
    5 4 
           Its type is:
    6 
    -        a1 :: TYPE r0
    7 
    -      Cannot unify ‘Any’ with the type variable ‘r0’
    5 
    +        a0 :: TYPE c0
    6 
    +      Cannot unify ‘Any’ with the type variable ‘c0’
    8 7 
           because the former is not a concrete ‘RuntimeRep’.
    9 8 
         • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’
    10 9 
           In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’

  • testsuite/tests/rep-poly/T23154.stderr
    ... ... @@ -8,3 +8,8 @@ T23154.hs:7:1: error: [GHC-52083]
    8 8 
         The first pattern in the equation for ‘f’
    9 9 
         cannot be assigned a fixed runtime representation, not even by defaulting.
    10 10 
         Suggested fix: Add a type signature.
    11 
    +
    12 
    +T23154.hs:7:1: error: [GHC-52083]
    13 
    +    The first pattern in the equation for ‘f’
    14 
    +    cannot be assigned a fixed runtime representation, not even by defaulting.
    15 
    +    Suggested fix: Add a type signature.

  • testsuite/tests/rep-poly/T23903.stderr
    1 
    -
    2 1 
     T23903.hs:21:1: error: [GHC-55287]
    3 2 
         • The first pattern in the equation for ‘f’
    4 3 
           does not have a fixed runtime representation.
    5 4 
           Its type is:
    6 
    -        t0 :: TYPE cx0
    7 
    -      Cannot unify ‘Rep a’ with the type variable ‘cx0’
    5 
    +        Unbox a :: TYPE c0
    6 
    +      Cannot unify ‘Rep a’ with the type variable ‘c0’
    8 7 
           because the former is not a concrete ‘RuntimeRep’.
    9 8 
         • The equation for ‘f’ has one visible argument,
    10 9 
             but its type ‘a #-> ()’ has none

  • testsuite/tests/simplCore/should_compile/simpl017.stderr
    1 
    -simpl017.hs:55:12: error: [GHC-46956]
    2 
    -    • Couldn't match type ‘v0’ with ‘v’
    3 
    -      Expected: [E m i] -> E' v m a
    4 
    -        Actual: [E m i] -> E' v0 m a
    5 
    -        because type variable ‘v’ would escape its scope
    6 
    -      This (rigid, skolem) type variable is bound by
    7 
    -        a type expected by the context:
    8 
    -          forall v. [E m i] -> E' v m a
    9 
    -        at simpl017.hs:55:12
    10 
    -    • In the first argument of ‘return’, namely ‘f’
    11 
    -      In a stmt of a 'do' block: return f
    1 
    +simpl017.hs:55:5: error: [GHC-83865]
    2 
    +    • Couldn't match type: [E m i] -> E' v0 m a
    3 
    +                     with: forall v. [E m i] -> E' v m a
    4 
    +      Expected: m (forall v. [E m i] -> E' v m a)
    5 
    +        Actual: m ([E m i] -> E' v0 m a)
    6 
    +    • In a stmt of a 'do' block: return f
    12 7 
           In the first argument of ‘E’, namely
    13 8 
             ‘(do let ix :: [E m i] -> m i
    14 9 
                      ix [i] = runE i
    15 10 
                      {-# INLINE f #-}
    16 11 
                      ....
    17 12 
                  return f)’
    13 
    +      In the expression:
    14 
    +        E (do let ix :: [E m i] -> m i
    15 
    +                  ix [i] = runE i
    16 
    +                  {-# INLINE f #-}
    17 
    +                  ....
    18 
    +              return f)
    18 19 
         • Relevant bindings include
    19 20 
             f :: [E m i] -> E' v0 m a (bound at simpl017.hs:54:9)
    21 
    +        ix :: [E m i] -> m i (bound at simpl017.hs:52:9)
    22 
    +        a :: arr i a (bound at simpl017.hs:50:11)
    23 
    +        liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a)
    24 
    +          (bound at simpl017.hs:50:1)
    20 25

  • testsuite/tests/typecheck/should_compile/T26030.hs
    1 
    +{-# LANGUAGE TypeFamilies #-}
    2 
    +{-# LANGUAGE GADTs #-}
    3 
    +
    4 
    +-- This program was rejected by GHC 9.12 due to a bug with
    5 
    +-- unification in QuickLook.
    6 
    +module T26030 where
    7 
    +
    8 
    +import Data.Kind
    9 
    +
    10 
    +type S :: Type -> Type
    11 
    +data S a where
    12 
    +  S1 :: S Bool
    13 
    +  S2 :: S Char
    14 
    +
    15 
    +type F :: Type -> Type
    16 
    +type family F a where
    17 
    +  F Bool = Bool
    18 
    +  F Char = Char
    19 
    +
    20 
    +foo :: forall a. S a -> IO (F a)
    21 
    +foo sa1 = do
    22 
    +  () <- return ()
    23 
    +  case sa1 of
    24 
    +    S1 -> return $ False
    25 
    +    S2 -> return 'x'

  • testsuite/tests/typecheck/should_compile/T27149.hs
    1 
    +{-# LANGUAGE TypeFamilies #-}
    2 
    +module T27149 where
    3 
    +
    4 
    +import Data.Kind (Type)
    5 
    +
    6 
    +type T :: Type -> Type
    7 
    +data T a where
    8 
    +  MkT :: T Bool
    9 
    +
    10 
    +type F :: Type -> Type
    11 
    +type family F a where
    12 
    +  F Bool = Int
    13 
    +
    14 
    +f :: IO (T a) -> (Bool -> Int) -> IO (F a)
    15 
    +f mt g = do
    16 
    +  t <- mt
    17 
    +  case t of
    18 
    +    MkT -> return $ g True

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -889,6 +889,8 @@ test('T21909', normal, compile, [''])
    889 889 
     test('T21909b', normal, compile, [''])
    890 890 
     test('T21443', normal, compile, [''])
    891 891 
     test('T22194', normal, compile, [''])
    892 
    +test('T26030', normal, compile, [''])
    893 
    +test('T27149', normal, compile, [''])
    892 894 
     test('QualifiedRecordUpdate',
    893 895 
         [ extra_files(['QualifiedRecordUpdate_aux.hs']) ]
    894 896 
         , multimod_compile, ['QualifiedRecordUpdate', '-v0'])

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