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

Commits:

11 changed files:

Changes:

  • compiler/GHC/Builtin/Types/Prim.hs
    ... ... @@ -1002,26 +1002,29 @@ doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName doubleRepDataConTy
    1002 1002
    1003 1003 
     Note [The equality types story]
    1004 1004 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1005 
    -GHC sports a veritable menagerie of equality types:
    1006 
    -
    1007 
    -         Type or  Lifted?  Hetero?  Role      Built in         Defining module
    1008 
    -         class?    L/U                        TyCon
    1009 
    ------------------------------------------------------------------------------------------
    1010 
    -~#         T        U      hetero   nominal   eqPrimTyCon      GHC.Prim
    1011 
    -~~         C        L      hetero   nominal   heqTyCon         GHC.Types
    1012 
    -~          C        L      homo     nominal   eqTyCon          GHC.Types
    1013 
    -:~:        T        L      homo     nominal   (not built-in)   Data.Type.Equality
    1014 
    -:~~:       T        L      hetero   nominal   (not built-in)   Data.Type.Equality
    1015 
    -
    1016 
    -~R#        T        U      hetero   repr      eqReprPrimTy     GHC.Prim
    1017 
    -Coercible  C        L      homo     repr      coercibleTyCon   GHC.Types
    1018 
    -Coercion   T        L      homo     repr      (not built-in)   Data.Type.Coercion
    1019 
    -~P#        T        U      hetero   phantom   eqPhantPrimTyCon GHC.Prim
    1005 
    +GHC sports a veritable menagerie of equality types.
    1006 
    +
    1007 
    +          Result kind    Hetero?  Role      Built in         Defining module
    1008 
    +---------------------------------------------------------------------------------
    1009 
    +~#        Constraint#    hetero   nominal   eqPrimTyCon      GHC.Prim
    1010 
    +~~        Constraint     hetero   nominal   heqTyCon         GHC.Types
    1011 
    +~         Constraint     homo     nominal   eqTyCon          GHC.Types
    1012 
    +:~:       Type           homo     nominal   (not built-in)   Data.Type.Equality
    1013 
    +:~~:      Type           hetero   nominal   (not built-in)   Data.Type.Equality
    1014 
    +
    1015 
    +~R#       Constraint#    hetero   repr      eqReprPrimTy     GHC.Prim
    1016 
    +Coercible Constraint     homo     repr      coercibleTyCon   GHC.Types
    1017 
    +Coercion  Type           homo     repr      (not built-in)   Data.Type.Coercion
    1018 
    +~P#       Constraint#    hetero   phantom   eqPhantPrimTyCon GHC.Prim
    1019 
    +
    1020 
    +Here `Constraint#` means `CONSTRAINT (TupleRep [])`, a constraint kind that is
    1021 
    +represented by a zero-width tuple.
    1020 1022
    1021 1023 
     Recall that "hetero" means the equality can related types of different
    1022 1024 
     kinds. Knowing that (t1 ~# t2) or (t1 ~R# t2) or even that (t1 ~P# t2)
    1023 1025 
     also means that (k1 ~# k2), where (t1 :: k1) and (t2 :: k2).
    1024 1026
    1027 
    +
    1025 1028 
     To produce less confusion for end users, when not dumping and without
    1026 1029 
     -fprint-equality-relations, each of these groups is printed as the bottommost
    1027 1030 
     listed equality. That is, (~#) and (~~) are both rendered as (~) in
    ... ... @@ -1030,7 +1033,7 @@ error messages, and (~R#) is rendered as Coercible.
    1030 1033 
     Let's take these one at a time:
    1031 1034
    1032 1035 
         --------------------------
    1033 
    -    (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
    1036 
    +    (~#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[])
    1034 1037 
         --------------------------
    1035 1038 
     This is The Type Of Equality in GHC. It classifies nominal coercions.
    1036 1039 
     This type is used in the solver for recording equality constraints.
    ... ... @@ -1054,8 +1057,6 @@ This is (almost) an ordinary class, defined as if by
    1054 1057 
     Here's what's unusual about it:
    1055 1058
    1056 1059 
      * We can't actually declare it that way because we don't have syntax for ~#.
    1057 
    -   And ~# isn't a constraint, so even if we could write it, it wouldn't kind
    1058 
    -   check.
    1059 1060
    1060 1061 
      * Users cannot write instances of it.
    1061 1062
    ... ... @@ -1112,7 +1113,7 @@ They are not defined within GHC at all.
    1112 1113
    1113 1114
    1114 1115 
         --------------------------
    1115 
    -    (~R#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
    1116 
    +    (~R#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[])
    1116 1117 
         --------------------------
    1117 1118 
     The is the representational analogue of ~#. This is the type of representational
    1118 1119 
     equalities that the solver works on. All wanted constraints of this type are
    ... ... @@ -1147,7 +1148,7 @@ within GHC at all.
    1147 1148
    1148 1149
    1149 1150 
         --------------------------
    1150 
    -    (~P#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
    1151 
    +    (~P#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[])
    1151 1152 
         --------------------------
    1152 1153 
     This is the phantom analogue of ~# and it is barely used at all.
    1153 1154 
     (The solver has no idea about this one.) Here is the motivation:

  • compiler/GHC/Core/Ppr.hs
    ... ... @@ -292,14 +292,14 @@ noParens :: SDoc -> SDoc
    292 292 
     noParens pp = pp
    293 293
    294 294 
     pprOptCo :: Coercion -> SDoc
    295 
    --- Print a coercion optionally; i.e. honouring -dsuppress-coercions
    296 
    -pprOptCo co = sdocOption sdocSuppressCoercions $ \case
    297 
    -              True  -> angleBrackets (text "Co:" <> int (coercionSize co)) <+> dcolon <+> co_type
    298 
    -              False -> parens $ sep [ppr co, dcolon <+> co_type]
    299 
    -    where
    300 
    -      co_type = sdocOption sdocSuppressCoercionTypes $ \case
    301 
    -          True  -> ellipsis
    302 
    -          False -> ppr (coercionType co)
    295 
    +-- Print a coercion with its type (unless suppressed by -dsuppress-coercion-types)
    296 
    +-- Honour -dsuppress-coercions
    297 
    +-- Placed here because it needs GHC.Core.Coercion.coercionType
    298 
    +pprOptCo co = sdocOption sdocSuppressCoercionTypes $ \case
    299 
    +               True  -> pprParendCo co
    300 
    +               False -> parens (sep [pprCo co, dcolon <+> pp_co_type])
    301 
    +  where
    302 
    +    pp_co_type = ppr (coercionType co)
    303 303
    304 304 
     ppr_id_occ :: (SDoc -> SDoc) -> Id -> SDoc
    305 305 
     ppr_id_occ add_par id

  • compiler/GHC/Core/TyCo/Ppr.hs
    ... ... @@ -132,8 +132,14 @@ tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
    132 132
    133 133 
     ------------
    134 134 
     pprCo, pprParendCo :: Coercion -> SDoc
    135 
    -pprCo       co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
    136 
    -pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
    135 
    +-- Print a coercion without its type
    136 
    +-- Honour -dsuppress-coercions
    137 
    +pprCo       co = sdocOption sdocSuppressCoercions $ \case
    138 
    +                 True  -> angleBrackets (text "Co:" <> int (coercionSize co))
    139 
    +                 False -> getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
    140 
    +pprParendCo co = sdocOption sdocSuppressCoercions $ \case
    141 
    +                 True  -> angleBrackets (text "Co:" <> int (coercionSize co))
    142 
    +                 False -> getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
    137 143
    138 144 
     tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
    139 145 
     tidyToIfaceCoSty co sty

  • compiler/GHC/Core/TyCo/Rep.hs
    ... ... @@ -1640,7 +1640,7 @@ Here,
    1640 1640 
       co3 = UnivCo ProofIrrelProv Nominal (CoercionTy co1) (CoercionTy co2) [co5]
    1641 1641 
       where
    1642 1642 
         co5 :: (a1 ~# Bool) ~# (a2 ~# Bool)
    1643 
    -    co5 = TyConAppCo Nominal (~#) [<Consraint#>, <Constraint#>, co4, <Bool>]
    1643 
    +    co5 = TyConAppCo Nominal (~#) [<Constraint#>, <Constraint#>, co4, <Bool>]
    1644 1644
    1645 1645
    1646 1646 
     Note [The importance of tracking UnivCo dependencies]

  • testsuite/tests/codeGen/should_compile/T25177.stderr
    ... ... @@ -11,7 +11,7 @@ lvl = foo d
    11 11
    12 12 
     bar1 = \ x eta -> case lvl of { W# ipv -> (# eta, () #) }
    13 13
    14 
    -bar = bar1 `cast` <Co:6> :: ...
    14 
    +bar = bar1 `cast` <Co:6>
    15 15
    16 16
    17 17

  • testsuite/tests/numeric/should_compile/T15547.stderr
    ... ... @@ -5,25 +5,25 @@ Result size of Tidy Core
    5 5
    6 6 
     nat2Word#
    7 7 
       = \ @n $dKnownNat p1 ->
    8 
    -      naturalToWord# ((natSing $dKnownNat) `cast` <Co:2> :: ...)
    8 
    +      naturalToWord# ((natSing $dKnownNat) `cast` <Co:2>)
    9 9
    10 10 
     foo = \ ds -> 18##
    11 11
    12 12 
     fd
    13 13 
       = \ @n $dKnownNat ds ->
    14 
    -      naturalToWord# ((natSing $dKnownNat) `cast` <Co:6> :: ...)
    14 
    +      naturalToWord# ((natSing $dKnownNat) `cast` <Co:6>)
    15 15
    16 16 
     d = \ ds -> 3##
    17 17
    18 18 
     fm
    19 19 
       = \ @n $dKnownNat ds ->
    20 
    -      naturalToWord# ((natSing $dKnownNat) `cast` <Co:8> :: ...)
    20 
    +      naturalToWord# ((natSing $dKnownNat) `cast` <Co:8>)
    21 21
    22 22 
     m = \ ds -> 9##
    23 23
    24 24 
     fp
    25 25 
       = \ @n $dKnownNat ds ->
    26 
    -      naturalToWord# ((natSing $dKnownNat) `cast` <Co:10> :: ...)
    26 
    +      naturalToWord# ((natSing $dKnownNat) `cast` <Co:10>)
    27 27
    28 28 
     p = \ ds -> 512##
    29 29

  • testsuite/tests/simplCore/should_compile/DataToTagFamilyScrut.stderr
    ... ... @@ -5,7 +5,7 @@ Result size of Tidy Core
    5 5
    6 6 
     testFun
    7 7 
       = \ @x v ->
    8 
    -      case v `cast` <Co:2> :: ... of {
    8 
    +      case v `cast` <Co:2> of {
    9 9 
             __DEFAULT -> 47#;
    10 10 
             C0 ipv -> -3#;
    11 11 
             C2 -> 13#;

  • testsuite/tests/simplCore/should_compile/T14978.stdout
    1 1 
     foo :: Goof Int
    2 
    -foo = T14978.Goof @Int @~<Co:1> :: Int GHC.Internal.Prim.~# Int
    2 
    +foo = T14978.Goof @Int @~(<Co:1> :: Int GHC.Internal.Prim.~# Int)

  • testsuite/tests/simplCore/should_compile/T18013.stderr
    ... ... @@ -161,11 +161,11 @@ T18013.$wmapMaybeRule
    161 161 
                          @s @(Maybe b) ww2 (GHC.Internal.Maybe.Nothing @b) #);
    162 162 
                   Just x ->
    163 163 
                     case ((wild s2 x)
    164 
    -                      `cast` <Co:4> :: IO (Result s b)
    165 
    -                                       ~R# (GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld
    166 
    -                                            -> (# GHC.Internal.Prim.State#
    167 
    -                                                    GHC.Internal.Prim.RealWorld,
    168 
    -                                                  Result s b #)))
    164 
    +                      `cast` (<Co:4>
    165 
    +                              :: IO (Result s b)
    166 
    +                                 ~R# (GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld
    167 
    +                                      -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld,
    168 
    +                                            Result s b #))))
    169 169 
                            s1
    170 170 
                     of
    171 171 
                     { (# ipv, ipv1 #) ->
    ... ... @@ -175,12 +175,13 @@ T18013.$wmapMaybeRule
    175 175 
                     }
    176 176 
                     }
    177 177 
                 })
    178 
    -         `cast` <Co:13> :: (s
    179 
    -                            -> Maybe a
    180 
    -                            -> GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld
    181 
    -                            -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld,
    182 
    -                                  Result s (Maybe b) #))
    183 
    -                           ~R# (s -> Maybe a -> IO (Result s (Maybe b))))
    178 
    +         `cast` (<Co:13>
    179 
    +                 :: (s
    180 
    +                     -> Maybe a
    181 
    +                     -> GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld
    182 
    +                     -> (# GHC.Internal.Prim.State# GHC.Internal.Prim.RealWorld,
    183 
    +                           Result s (Maybe b) #))
    184 
    +                    ~R# (s -> Maybe a -> IO (Result s (Maybe b)))))
    184 185 
           }
    185 186 
           }
    186 187

  • testsuite/tests/simplCore/should_compile/T24229a.stderr
    ... ... @@ -15,8 +15,8 @@ foo
    15 15 
       = \ @a ds ds1 ->
    16 16 
           case ds of { I# ww ->
    17 17 
           case ww of ds2 {
    18 
    -        __DEFAULT -> case ds1 `cast` <Co:4> :: ... of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } };
    19 
    -        0# -> Just (ds1 `cast` <Co:4> :: ...)
    18 
    +        __DEFAULT -> case ds1 `cast` <Co:4> of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } };
    19 
    +        0# -> Just (ds1 `cast` <Co:4>)
    20 20 
           }
    21 21 
           }
    22 22

  • testsuite/tests/simplCore/should_compile/T24229b.stderr
    ... ... @@ -15,8 +15,8 @@ foo
    15 15 
       = \ @a ds ds1 ->
    16 16 
           case ds of { I# ww ->
    17 17 
           case ww of ds2 {
    18 
    -        __DEFAULT -> case ds1 `cast` <Co:4> :: ... of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } };
    19 
    -        0# -> Just (ds1 `cast` <Co:4> :: ...)
    18 
    +        __DEFAULT -> case ds1 `cast` <Co:4> of { (x, y) -> case foo_$s$wfoo (-# ds2 1#) y x of { (# ww1 #) -> Just ww1 } };
    19 
    +        0# -> Just (ds1 `cast` <Co:4>)
    20 20 
           }
    21 21 
           }
    22 22

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