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

Commits:

6 changed files:

Changes:

  • compiler/GHC/Core/Coercion.hs
    ... ... @@ -93,9 +93,10 @@ module GHC.Core.Coercion (
    93 93 
             liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
    94 94 
             emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
    95 95 
             liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst,
    96 
    +        updateLCSubst,
    96 97
    97 98 
             mkSubstLiftingContext, liftingContextSubst, zapLiftingContext,
    98 
    -        substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet,
    99 
    +        lcLookupCoVar, lcInScopeSet,
    99 100
    100 101 
             LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
    101 102 
             substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
    ... ... @@ -2136,15 +2137,11 @@ extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
    2136 2137 
     zapLiftingContext :: LiftingContext -> LiftingContext
    2137 2138 
     zapLiftingContext (LC subst _) = LC (zapSubst subst) emptyVarEnv
    2138 2139
    2139 
    --- | Like 'substForAllCoBndr', but works on a lifting context
    2140 
    -substForAllCoBndrUsingLC :: SwapFlag
    2141 
    -                         -> (Coercion -> Coercion)
    2142 
    -                         -> LiftingContext -> TyCoVar -> Coercion
    2143 
    -                         -> (LiftingContext, TyCoVar, Coercion)
    2144 
    -substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
    2145 
    -  = (LC subst' lc_env, tv', co')
    2140 
    +updateLCSubst :: LiftingContext -> (Subst -> (Subst, a)) -> (LiftingContext, a)
    2141 
    +-- Lift a Subst-update function over LiftingContext
    2142 
    +updateLCSubst (LC subst lc_env) upd = (LC subst' lc_env, res)
    2146 2143 
       where
    2147 
    -    (subst', tv', co') = substForAllCoBndrUsing sym sco subst tv co
    2144 
    +    (subst', res) = upd subst
    2148 2145
    2149 2146 
     -- | The \"lifting\" operation which substitutes coercions for type
    2150 2147 
     --   variables in a type to produce a coercion.

  • compiler/GHC/Core/Coercion/Opt.hs
    ... ... @@ -358,12 +358,12 @@ opt_co4' env sym rep r (AppCo co1 co2)
    358 358 
                 (opt_co4 env sym False Nominal co2)
    359 359
    360 360 
     opt_co4' env sym rep r (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
    361 
    -                                , fco_kind = k_co, fco_body = co })
    362 
    -  = case optForAllCoBndr env sym tv k_co of
    363 
    -      (env', tv', k_co') -> mkForAllCo tv' visL' visR' k_co' $
    364 
    -                            opt_co4 env' sym rep r co
    361 
    +                                 , fco_kind = k_co, fco_body = co })
    362 
    +  = mkForAllCo tv' visL' visR' k_co' $
    363 
    +    opt_co4 env' sym rep r co
    365 364 
          -- Use the "mk" functions to check for nested Refls
    366 365 
       where
    366 
    +    !(env', tv', k_co') = optForAllCoBndr env sym tv k_co
    367 367 
         !(visL', visR') = swapSym sym (visL, visR)
    368 368
    369 369 
     opt_co4' env sym rep r (FunCo _r afl afr cow co1 co2)
    ... ... @@ -1401,10 +1401,68 @@ and these two imply
    1401 1401
    1402 1402 
     -}
    1403 1403
    1404 
    +{- Note [Optimising ForAllCo]
    1405 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1406 
    +If sym=NotSwapped, optimising ForAllCo is relatively easy:
    1407 
    +   opt env (ForAllCo tcv kco bodyco)
    1408 
    +     = ForAllCo tcv' (opt env kco) (opt env' bodyco)
    1409 
    +     where
    1410 
    +       (env', tcv') = substBndr env tcv
    1411 
    +
    1412 
    +Just apply the substitution to the kind of the binder, deal with
    1413 
    +shadowing etc, and recurse.  Remember in (ForAllCo tcv kco bodyco)
    1414 
    +    varKind tcv = coercionLKind kco
    1415 
    +
    1416 
    +But if sym=Swapped, things are trickier.  Here is an identity that helps:
    1417 
    +   Sym (ForAllCo (tv:k1) (kco:k1~k2) bodyco)
    1418 
    +   = ForAllCo (tv:k2) (Sym kco : k2~k1)
    1419 
    +              (Sym (bodyco[tv:->tv:k2 |> Sym kco]))
    1420 
    +
    1421 
    +* We re-type tv:k1 to become tv:k2.
    1422 
    +* We push Sym into kco
    1423 
    +* We push Sym into bodyco
    1424 
    +* BUT we must /also/ remember to replace all occurrences of
    1425 
    +      of tv:k1 in bodyco by (tv:k2 |> Sym kco)
    1426 
    +  This mirrors what happens in the typing rule for ForAllCo
    1427 
    +  See Note [ForAllCo] in GHC.Core.TyCo.Rep
    1428 
    +
    1429 
    +-}
    1404 1430 
     optForAllCoBndr :: LiftingContext -> SwapFlag
    1405 
    -                -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
    1406 
    -optForAllCoBndr env sym
    1407 
    -  = substForAllCoBndrUsingLC sym (opt_co4 env sym False Nominal) env
    1431 
    +                -> TyCoVar -> Coercion
    1432 
    +                -> (LiftingContext, TyCoVar, Coercion)
    1433 
    +-- See Note [Optimising ForAllCo]
    1434 
    +optForAllCoBndr env sym tcv kco
    1435 
    +  = (env', tcv', kco')
    1436 
    +  where
    1437 
    +    kco' = opt_co4 env sym False Nominal kco  -- Push sym into kco
    1438 
    +    (env', tcv') = updateLCSubst env upd_subst
    1439 
    +
    1440 
    +    upd_subst :: Subst -> (Subst, TyCoVar)
    1441 
    +    upd_subst subst
    1442 
    +      | isTyVar tcv = upd_subst_tv subst
    1443 
    +      | otherwise   = upd_subst_cv subst
    1444 
    +
    1445 
    +    upd_subst_tv subst
    1446 
    +      | notSwapped sym || isReflCo kco' = (subst1, tv1)
    1447 
    +      | otherwise                       = (subst2, tv2)
    1448 
    +      where
    1449 
    +        -- subst1,tv1: apply the substitution to the binder and its kind
    1450 
    +        -- NB: varKind tv = coercionLKind kco
    1451 
    +        (subst1, tv1) = substTyVarBndr subst tcv
    1452 
    +        -- In the Swapped case, we re-kind the type variable, AND
    1453 
    +        -- override the substitution for the original variable to the
    1454 
    +        -- re-kinded one, suitably casted
    1455 
    +        tv2    = tv1 `setTyVarKind` coercionLKind kco'
    1456 
    +        subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` kco'))
    1457 
    +                 `extendSubstInScope` tv2
    1458 
    +
    1459 
    +    upd_subst_cv subst   -- ToDo: probably not right yet
    1460 
    +      | notSwapped sym || isReflCo kco' = (subst1, cv1)
    1461 
    +      | otherwise                       = (subst2, cv2)
    1462 
    +      where
    1463 
    +        (subst1, cv1) = substCoVarBndr subst tcv
    1464 
    +        cv2    = cv1 `setTyVarKind` coercionLKind kco'
    1465 
    +        subst2 = subst1 `extendSubstInScope` cv2
    1408 1466
    1409 1467
    1410 1468 
     {- **********************************************************************

  • compiler/GHC/Core/TyCo/Subst.hs
    ... ... @@ -60,7 +60,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
    60 60 
        , mkAxiomCo, mkAppCo, mkGReflCo
    61 61 
        , mkInstCo, mkLRCo, mkTyConAppCo
    62 62 
        , mkCoercionType
    63 
    -   , coercionKind, coercionLKind, coVarTypesRole )
    63 
    +   , coercionLKind, coVarTypesRole )
    64 64 
     import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
    65 65 
     import {-# SOURCE #-} GHC.Core.Ppr ( ) -- instance Outputable CoreExpr
    66 66 
     import {-# SOURCE #-} GHC.Core ( CoreExpr )
    ... ... @@ -68,12 +68,10 @@ import {-# SOURCE #-} GHC.Core ( CoreExpr )
    68 68 
     import GHC.Core.TyCo.Rep
    69 69 
     import GHC.Core.TyCo.FVs
    70 70
    71 
    -import GHC.Types.Basic( SwapFlag(..), isSwapped, pickSwap, notSwapped )
    72 71 
     import GHC.Types.Var
    73 72 
     import GHC.Types.Var.Set
    74 73 
     import GHC.Types.Var.Env
    75 74
    76 
    -import GHC.Data.Pair
    77 75 
     import GHC.Utils.Constants (debugIsOn)
    78 76 
     import GHC.Utils.Misc
    79 77 
     import GHC.Types.Unique.Supply
    ... ... @@ -922,7 +920,7 @@ substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $
    922 920 
     substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
    923 921 
                       -> (Subst, TyCoVar, Coercion)
    924 922 
     substForAllCoBndr subst
    925 
    -  = substForAllCoBndrUsing NotSwapped (substCo subst) subst
    923 
    +  = substForAllCoBndrUsing (substCo subst) subst
    926 924
    927 925 
     -- | Like 'substForAllCoBndr', but disables sanity checks.
    928 926 
     -- The problems that the sanity checks in substCo catch are described in
    ... ... @@ -932,33 +930,26 @@ substForAllCoBndr subst
    932 930 
     substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion
    933 931 
                                -> (Subst, TyCoVar, Coercion)
    934 932 
     substForAllCoBndrUnchecked subst
    935 
    -  = substForAllCoBndrUsing NotSwapped (substCoUnchecked subst) subst
    933 
    +  = substForAllCoBndrUsing (substCoUnchecked subst) subst
    936 934
    937 935 
     -- See Note [Sym and ForAllCo]
    938 
    -substForAllCoBndrUsing :: SwapFlag  -- Apply sym to binder?
    939 
    -                       -> (Coercion -> Coercion)  -- transformation to kind co
    936 
    +substForAllCoBndrUsing :: (Coercion -> Coercion)  -- transformation to kind co
    940 937 
                            -> Subst -> TyCoVar -> KindCoercion
    941 938 
                            -> (Subst, TyCoVar, KindCoercion)
    942 
    -substForAllCoBndrUsing sym sco subst old_var
    943 
    -  | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var
    944 
    -  | otherwise       = substForAllCoCoVarBndrUsing sym sco subst old_var
    939 
    +substForAllCoBndrUsing sco subst old_var
    940 
    +  | isTyVar old_var = substForAllCoTyVarBndrUsing sco subst old_var
    941 
    +  | otherwise       = substForAllCoCoVarBndrUsing sco subst old_var
    945 942
    946 
    -substForAllCoTyVarBndrUsing :: SwapFlag  -- Apply sym to binder?
    947 
    -                            -> (Coercion -> Coercion)  -- transformation to kind co
    943 
    +substForAllCoTyVarBndrUsing :: (Coercion -> Coercion)  -- transformation to kind co
    948 944 
                                 -> Subst -> TyVar -> KindCoercion
    949 945 
                                 -> (Subst, TyVar, KindCoercion)
    950 
    -substForAllCoTyVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) old_var old_kind_co
    946 
    +substForAllCoTyVarBndrUsing sco (Subst in_scope idenv tenv cenv) old_var old_kind_co
    951 947 
       = assert (isTyVar old_var )
    952 948 
         ( Subst (in_scope `extendInScopeSet` new_var) idenv new_env cenv
    953 949 
         , new_var, new_kind_co )
    954 950 
       where
    955 
    -    new_env | no_change, notSwapped sym
    956 
    -            = delVarEnv tenv old_var
    957 
    -            | isSwapped sym
    958 
    -            = extendVarEnv tenv old_var $
    959 
    -              TyVarTy new_var `CastTy` new_kind_co
    960 
    -            | otherwise
    961 
    -            = extendVarEnv tenv old_var (TyVarTy new_var)
    951 
    +    new_env | no_change = delVarEnv tenv old_var
    952 
    +            | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
    962 953
    963 954 
         no_kind_change = noFreeVarsOfCo old_kind_co
    964 955 
         no_change = no_kind_change && (new_var == old_var)
    ... ... @@ -974,20 +965,17 @@ substForAllCoTyVarBndrUsing sym sco (Subst in_scope idenv tenv cenv) old_var old
    974 965
    975 966 
         new_var  = uniqAway in_scope (setTyVarKind old_var new_ki1)
    976 967
    977 
    -substForAllCoCoVarBndrUsing :: SwapFlag  -- Apply sym to binder?
    978 
    -                            -> (Coercion -> Coercion)  -- transformation to kind co
    968 
    +substForAllCoCoVarBndrUsing :: (Coercion -> Coercion)  -- transformation to kind co
    979 969 
                                 -> Subst -> CoVar -> KindCoercion
    980 970 
                                 -> (Subst, CoVar, KindCoercion)
    981 
    -substForAllCoCoVarBndrUsing sym sco (Subst in_scope idenv tenv cenv)
    971 
    +substForAllCoCoVarBndrUsing sco (Subst in_scope idenv tenv cenv)
    982 972 
                                 old_var old_kind_co
    983 973 
       = assert (isCoVar old_var )
    984 974 
         ( Subst (in_scope `extendInScopeSet` new_var) idenv tenv new_cenv
    985 975 
         , new_var, new_kind_co )
    986 976 
       where
    987 
    -    new_cenv | no_change, notSwapped sym
    988 
    -             = delVarEnv cenv old_var
    989 
    -             | otherwise
    990 
    -             = extendVarEnv cenv old_var (mkCoVarCo new_var)
    977 
    +    new_cenv | no_change = delVarEnv cenv old_var
    978 
    +             | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
    991 979
    992 980 
         no_kind_change = noFreeVarsOfCo old_kind_co
    993 981 
         no_change = no_kind_change && (new_var == old_var)
    ... ... @@ -995,10 +983,8 @@ substForAllCoCoVarBndrUsing sym sco (Subst in_scope idenv tenv cenv)
    995 983 
         new_kind_co | no_kind_change = old_kind_co
    996 984 
                     | otherwise      = sco old_kind_co
    997 985
    998 
    -    Pair h1 h2 = coercionKind new_kind_co
    999 
    -
    1000 
    -    new_var       = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type
    1001 
    -    new_var_type  = pickSwap sym h1 h2
    986 
    +    new_ki1       = coercionLKind new_kind_co
    987 
    +    new_var       = uniqAway in_scope $ mkCoVar (varName old_var) new_ki1
    1002 988
    1003 989 
     substCoVar :: Subst -> CoVar -> Coercion
    1004 990 
     substCoVar (Subst _ _ _ cenv) cv

  • compiler/GHC/Core/Type.hs
    ... ... @@ -559,11 +559,7 @@ expandTypeSynonyms ty
    559 559 
         go_co _ (HoleCo h)
    560 560 
           = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
    561 561
    562 
    -      -- the "False" and "const" are to accommodate the type of
    563 
    -      -- substForAllCoBndrUsing, which is general enough to
    564 
    -      -- handle coercion optimization (which sometimes swaps the
    565 
    -      -- order of a coercion)
    566 
    -    go_cobndr subst = substForAllCoBndrUsing NotSwapped (go_co subst) subst
    562 
    +    go_cobndr subst = substForAllCoBndrUsing (go_co subst) subst
    567 563
    568 564 
     {- Notes on type synonyms
    569 565 
     ~~~~~~~~~~~~~~~~~~~~~~~~~

  • testsuite/tests/typecheck/should_compile/T26345.hs
    1 
    +{-# LANGUAGE GHC2021 #-}
    2 
    +{-# LANGUAGE DataKinds #-}
    3 
    +{-# LANGUAGE TypeAbstractions #-}
    4 
    +{-# LANGUAGE TypeFamilies #-}
    5 
    +module Bug where
    6 
    +
    7 
    +import Data.Kind (Constraint, Type)
    8 
    +
    9 
    +type Sing :: k -> Type
    10 
    +type family Sing @k
    11 
    +
    12 
    +type Tuple0 :: Type
    13 
    +data Tuple0 = MkTuple0
    14 
    +
    15 
    +type STuple0 :: Tuple0 -> Type
    16 
    +data STuple0 z where
    17 
    +  SMkTuple0 :: STuple0 MkTuple0
    18 
    +type instance Sing @Tuple0 = STuple0
    19 
    +
    20 
    +type U1 :: Type
    21 
    +data U1 = MkU1
    22 
    +
    23 
    +type SU1 :: U1 -> Type
    24 
    +data SU1 z where
    25 
    +  SMkU1 :: SU1 MkU1
    26 
    +type instance Sing @U1 = SU1
    27 
    +
    28 
    +type Generic :: Type -> Constraint
    29 
    +class Generic a where
    30 
    +  type Rep a :: Type
    31 
    +
    32 
    +type PGeneric :: Type -> Constraint
    33 
    +class PGeneric a where
    34 
    +  type PFrom (x :: a)     :: Rep a
    35 
    +
    36 
    +type SGeneric :: Type -> Constraint
    37 
    +class SGeneric a where
    38 
    +  sFrom :: forall (x :: a). Sing x -> Sing (PFrom x)
    39 
    +
    40 
    +instance SGeneric Tuple0 where
    41 
    +  sFrom SMkTuple0 = SMkU1
    42 
    +
    43 
    +instance Generic Tuple0 where
    44 
    +  type Rep Tuple0 = U1
    45 
    +
    46 
    +instance PGeneric Tuple0 where
    47 
    +  type PFrom MkTuple0  = MkU1
    48 
    +
    49 
    +type SDecide :: Type -> Constraint
    50 
    +class SDecide a where
    51 
    +  sDecide :: forall (x :: a) (y :: a). Sing x -> Sing y -> Bool
    52 
    +
    53 
    +instance SDecide U1 where
    54 
    +  sDecide SMkU1 SMkU1 = True
    55 
    +
    56 
    +sDecideDefault :: Sing MkTuple0 -> Sing MkTuple0 -> Bool
    57 
    +sDecideDefault s1 s2 = sDecide (sFrom s1) (sFrom s2)

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -948,3 +948,5 @@ test('T26256a', normal, compile, [''])
    948 948 
     test('T25992a', normal, compile, [''])
    949 949 
     test('T26346', normal, compile, [''])
    950 950 
     test('T26358', expect_broken(26358), compile, [''])
    951 
    +test('T26345', normal, compile, [''])
    952 
    +

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