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

Commits:

6 changed files:

Changes:

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -1098,7 +1098,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1098 1098 
       them.  This is done in can_eq_nc.  Of course, we can't unwrap if the data
    1099 1099 
       constructor isn't in scope.  See Note [Unwrap newtypes first].
    1100 1100
    1101 
    -* Incompleteness example (EX2): see #24887
    1101 
    +* Incompleteness example (EX2): prioritise Nominal equalities. See #24887
    1102 1102 
           data family D a
    1103 1103 
           data instance D Int  = MkD1 (D Char)
    1104 1104 
           data instance D Bool = MkD2 (D Char)
    ... ... @@ -1116,7 +1116,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1116 1116 
       CONCLUSION: prioritise nominal equalites in the work list.
    1117 1117 
       See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet.
    1118 1118
    1119 
    -* Incompleteness example (EX3): available Givens
    1119 
    +* Incompleteness example (EX3): check available Givens
    1120 1120 
           newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
    1121 1121 
           type role Nt representational  -- but the user gives it an R role anyway
    1122 1122
    ... ... @@ -1134,36 +1134,41 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1134 1134 
       equalities that could later solve it.
    1135 1135
    1136 1136 
       But what precisely does it mean to say "any Given equalities that could
    1137 
    -  later solve it"?
    1138 
    -
    1139 
    -  In #22924 we had
    1140 
    -     [G] f a ~R# a     [W] Const (f a) a ~R# Const a a
    1141 
    -  where Const is an abstract newtype.  If we decomposed the newtype, we
    1142 
    -  could solve.  Not-decomposing on the grounds that (f a ~R# a) might turn
    1143 
    -  into (Const (f a) a ~R# Const a a) seems a bit silly.
    1144 
    -
    1145 
    -  In #22331 we had
    1146 
    -     [G] N a ~R# N b   [W] N b ~R# N a
    1147 
    -  (where N is abstract so we can't unwrap). Here we really /don't/ want to
    1148 
    -  decompose, because the /only/ way to solve the Wanted is from that Given
    1149 
    -  (with a Sym).
    1150 
    -
    1151 
    -  In #22519 we had
    1152 
    -     [G] a <= b     [W] IO Age ~R# IO Int
    1153 
    -
    1154 
    -  (where IO is abstract so we can't unwrap, and newtype Age = Int; and (<=)
    1155 
    -  is a type-level comparison on Nats).  Here we /must/ decompose, despite the
    1156 
    -  existence of an Irred Given, or we will simply be stuck.  (Side note: We
    1157 
    -  flirted with deep-rewriting of newtypes (see discussion on #22519 and
    1158 
    -  !9623) but that turned out not to solve #22924, and also makes type
    1159 
    -  inference loop more often on recursive newtypes.)
    1137 
    +  later solve it"?  It's tricky!
    1138 
    +
    1139 
    +  * In #22924 we had
    1140 
    +       [G] f a ~R# a     [W] Const (f a) a ~R# Const a a
    1141 
    +    where Const is an abstract newtype.  If we decomposed the newtype, we
    1142 
    +    could solve.  Not-decomposing on the grounds that (f a ~R# a) might turn
    1143 
    +    into (Const (f a) a ~R# Const a a) seems a bit silly.
    1144 
    +
    1145 
    +  * In #22331 we had
    1146 
    +       [G] N a ~R# N b   [W] N b ~R# N a
    1147 
    +    (where N is abstract so we can't unwrap). Here we really /don't/ want to
    1148 
    +    decompose, because the /only/ way to solve the Wanted is from that Given
    1149 
    +    (with a Sym).
    1150 
    +
    1151 
    +  * In #22519 we had
    1152 
    +       [G] a <= b     [W] IO Age ~R# IO Int
    1153 
    +
    1154 
    +    (where IO is abstract so we can't unwrap, and newtype Age = Int; and (<=)
    1155 
    +    is a type-level comparison on Nats).  Here we /must/ decompose, despite the
    1156 
    +    existence of an Irred Given, or we will simply be stuck.  (Side note: We
    1157 
    +    flirted with deep-rewriting of newtypes (see discussion on #22519 and
    1158 
    +    !9623) but that turned out not to solve #22924, and also makes type
    1159 
    +    inference loop more often on recursive newtypes.)
    1160 
    +
    1161 
    +  * In #26020 we had a /quantified/ constraint
    1162 
    +        forall x. Coercible (N t1) (N t2)
    1163 
    +    and (roughly) [W] N t1 ~R# N t2
    1164 
    +    That quantified constraint can solve the Wanted, so don't decompose!
    1160 1165
    1161 1166 
       The currently-implemented compromise is this:
    1162 
    -
    1163 
    -    we decompose [W] N s ~R# N t unless there is a [G] N s' ~ N t'
    1164 
    -
    1165 
    -  that is, a Given Irred equality with both sides headed with N.
    1166 
    -  See the call to noGivenNewtypeReprEqs in canTyConApp.
    1167 
    +       We decompose [W] N s ~R# N t unless there is
    1168 
    +       - an Irred [G] N s' ~ N t'
    1169 
    +       - a quantified [G] forall ... => N s' ~ N t'
    1170 
    +       that is, a Given equality with both sides headed with N.
    1171 
    +  See the call to `noGivenNewtypeReprEqs` in `canTyConApp`.
    1167 1172
    1168 1173 
       This is not perfect.  In principle a Given like [G] (a b) ~ (c d), or
    1169 1174 
       even just [G] c, could later turn into N s ~ N t.  But since the free
    ... ... @@ -1174,7 +1179,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
    1174 1179 
       un-expanded equality superclasses; but only in some very obscure
    1175 1180 
       recursive-superclass situations.
    1176 1181
    1177 
    -   Yet another approach (!) is desribed in
    1182 
    +   Yet another approach (!) is described in
    1178 1183 
        Note [Decomposing newtypes a bit more aggressively].
    1179 1184
    1180 1185 
     Remember: decomposing Wanteds is always /sound/. This Note is

  • compiler/GHC/Tc/Solver/InertSet.hs
    ... ... @@ -70,7 +70,7 @@ import GHC.Core.Predicate
    70 70 
     import qualified GHC.Core.TyCo.Rep as Rep
    71 71 
     import GHC.Core.TyCon
    72 72 
     import GHC.Core.Class( classTyCon )
    73 
    -import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey )
    73 
    +import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey, coercibleTyConKey )
    74 74 
     import GHC.Utils.Misc       ( partitionWith )
    75 75 
     import GHC.Utils.Outputable
    76 76 
     import GHC.Utils.Panic
    ... ... @@ -1862,21 +1862,34 @@ isOuterTyVar tclvl tv
    1862 1862 
       | otherwise  = False  -- Coercion variables; doesn't much matter
    1863 1863
    1864 1864 
     noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
    1865 
    --- True <=> there is no Irred looking like (N tys1 ~ N tys2)
    1866 
    --- See Note [Decomposing newtype equalities] (EX2) in GHC.Tc.Solver.Equality
    1867 
    ---     This is the only call site.
    1868 
    -noGivenNewtypeReprEqs tc inerts
    1869 
    -  = not (anyBag might_help (inert_irreds (inert_cans inerts)))
    1865 
    +-- True <=> there is no Given looking like (N tys1 ~ N tys2)
    1866 
    +-- See Note [Decomposing newtype equalities] (EX3) in GHC.Tc.Solver.Equality
    1867 
    +noGivenNewtypeReprEqs tc (IS { inert_cans = inerts })
    1868 
    +  | IC { inert_irreds = irreds, inert_insts = quant_cts } <- inerts
    1869 
    +  = not (anyBag might_help_irred irreds || any might_help_qc quant_cts)
    1870 
    +    -- Look in both inert_irreds /and/ inert_insts (#26020)
    1870 1871 
       where
    1871 
    -    might_help irred
    1872 
    -      = case classifyPredType (ctEvPred (irredCtEvidence irred)) of
    1873 
    -          EqPred ReprEq t1 t2
    1874 
    -             | Just (tc1,_) <- tcSplitTyConApp_maybe t1
    1875 
    -             , tc == tc1
    1876 
    -             , Just (tc2,_) <- tcSplitTyConApp_maybe t2
    1877 
    -             , tc == tc2
    1878 
    -             -> True
    1879 
    -          _  -> False
    1872 
    +    might_help_irred (IrredCt { ir_ev = ev })
    1873 
    +      | EqPred ReprEq t1 t2 <- classifyPredType (ctEvPred ev)
    1874 
    +      = headed_by_tc t1 t2
    1875 
    +      | otherwise
    1876 
    +      = False
    1877 
    +
    1878 
    +    might_help_qc (QCI { qci_body = pred })
    1879 
    +      | ClassPred cls [_, t1, t2] <- classifyPredType pred
    1880 
    +      , cls `hasKey` coercibleTyConKey
    1881 
    +      = headed_by_tc t1 t2
    1882 
    +      | otherwise
    1883 
    +      = False
    1884 
    +
    1885 
    +    headed_by_tc t1 t2
    1886 
    +      | Just (tc1,_) <- tcSplitTyConApp_maybe t1
    1887 
    +      , tc == tc1
    1888 
    +      , Just (tc2,_) <- tcSplitTyConApp_maybe t2
    1889 
    +      , tc == tc2
    1890 
    +      = True
    1891 
    +      | otherwise
    1892 
    +      = False
    1880 1893
    1881 1894 
     -- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@?
    1882 1895 
     --

  • testsuite/tests/typecheck/should_compile/T26020.hs
    1 
    +{-# LANGUAGE TypeFamilies #-}
    2 
    +{-# LANGUAGE QuantifiedConstraints #-}
    3 
    +
    4 
    +module T26020 where
    5 
    +
    6 
    +import Data.Kind
    7 
    +import Data.Coerce
    8 
    +
    9 
    +class C r where
    10 
    +  data T r :: Type -> Type
    11 
    +
    12 
    +-- type family F r
    13 
    +-- data T r i = MkR r (F i)
    14 
    +
    15 
    +coT :: (forall x. Coercible (T r i) (T r o))
    16 
    +    => T r i -> T r o
    17 
    +coT = coerce

  • testsuite/tests/typecheck/should_compile/T26020a.hs
    1 
    +{-# LANGUAGE QuantifiedConstraints #-}
    2 
    +module T26020a where
    3 
    +
    4 
    +import T26020a_help( N ) -- Not the MkN constructor
    5 
    +import Data.Coerce
    6 
    +
    7 
    +coT :: (forall x. Coercible (N i) (N o))
    8 
    +    => N i -> N o
    9 
    +coT = coerce

  • testsuite/tests/typecheck/should_compile/T26020a_help.hs
    1 
    +{-# LANGUAGE TypeFamilies #-}
    2 
    +
    3 
    +module T26020a_help where
    4 
    +
    5 
    +type family F a
    6 
    +newtype N a = MkN (F a)
    7 
    +

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -938,3 +938,5 @@ test('T25266a', normal, compile_fail, [''])
    938 938 
     test('T25266b', normal, compile, [''])
    939 939 
     test('T25597', normal, compile, [''])
    940 940 
     test('T25960', normal, compile, [''])
    941 
    +test('T26020', normal, compile, [''])
    942 
    +test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0'])

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