Commit daf1eee4 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Clarify some comments around injectivity.

parent a6b8b9c2
......@@ -720,7 +720,9 @@ NthCo on representational coercions over newtypes. NthCo comes into play
only when decomposing givens. So we avoid decomposing representational given
equalities over newtypes.
But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes, as
But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes --
it's the only way we could ever prove (IO Int ~R IO Age), recalling that IO
is a newtype. However, we must decompose wanteds only as
long as there are no Givens that might (later) influence Coercible solving.
(See Note [Instance and Given overlap] in TcInteract.) By the time we reach
canDecomposableTyConApp, we know that any newtypes that can be unwrapped have
......@@ -743,6 +745,20 @@ evidence that (Nt Int ~R Nt Char), even if we can't form that evidence in this
module (because Mk is not in scope). Creating this scenario in source Haskell
is challenging; there is no test case.
Example of how decomposing a wanted newtype is wrong, if it's not the only
possibility:
newtype Nt a = MkNt (Id a)
type family Id a where Id a = a
[W] Nt Int ~R Nt Age
Because of its use of a type family, Nt's parameter will get inferred to have
a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
is unsatisfiable. Unwrapping, though, leads to a solution.
In summary, decomposing a wanted is always sound, but it might not be complete.
So we do it when it's the only possible way forward.
Note [Decomposing equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -814,7 +830,8 @@ implementation is indeed merged.)
{2}: See Note [Decomposing newtypes]
{3}: Because of the possibility of newtype instances, we must treat data families
like newtypes. See also Note [Decomposing newtypes].
like newtypes. See also Note [Decomposing newtypes]. See #10534 and test case
typecheck/should_fail/T10534.
{4}: Because type variables can stand in for newtypes, we conservatively do not
decompose AppTys over representational equality.
......
......@@ -996,7 +996,7 @@ checkBootTyCon tc1 tc2
quotes (text "representational") <+> text "in boot files.")
eqAlgRhs tc (AbstractTyCon dis1) rhs2
| dis1 = check (isDistinctAlgRhs rhs2) --Check compatibility
| dis1 = check (isGenInjAlgRhs rhs2) --Check compatibility
(text "The natures of the declarations for" <+>
quotes (ppr tc) <+> text "are different")
| otherwise = checkSuccess
......
......@@ -49,7 +49,7 @@ module TyCon(
isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
isBuiltInSynFamTyCon_maybe,
isUnLiftedTyCon,
isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isDistinctAlgRhs,
isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
isTyConAssoc, tyConAssoc_maybe,
isRecursiveTyCon,
isImplicitTyCon,
......@@ -1165,7 +1165,7 @@ isAbstractTyCon _ = False
-- algebraic
makeTyConAbstract :: TyCon -> TyCon
makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs })
= tc { algTcRhs = AbstractTyCon (isDistinctAlgRhs rhs) }
= tc { algTcRhs = AbstractTyCon (isGenInjAlgRhs rhs) }
makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
-- | Does this 'TyCon' represent something that cannot be defined in Haskell?
......@@ -1214,12 +1214,13 @@ isDataTyCon _ = False
-- (where X is the role passed in):
-- If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
-- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
-- See also Note [Decomposing equalities] in TcCanonical
isInjectiveTyCon :: TyCon -> Role -> Bool
isInjectiveTyCon _ Phantom = False
isInjectiveTyCon (FunTyCon {}) _ = True
isInjectiveTyCon (AlgTyCon {}) Nominal = True
isInjectiveTyCon (AlgTyCon {algTcRhs = rhs}) Representational
= isDistinctAlgRhs rhs
= isGenInjAlgRhs rhs
isInjectiveTyCon (SynonymTyCon {}) _ = False
isInjectiveTyCon (FamilyTyCon {}) _ = False
isInjectiveTyCon (PrimTyCon {}) _ = True
......@@ -1230,6 +1231,7 @@ isInjectiveTyCon (PromotedTyCon {ty_con = tc}) r
-- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
-- (where X is the role passed in):
-- If (T tys ~X t), then (t's head ~X T).
-- See also Note [Decomposing equalities] in TcCanonical
isGenerativeTyCon :: TyCon -> Role -> Bool
isGenerativeTyCon = isInjectiveTyCon
-- as it happens, generativity and injectivity coincide, but there's
......@@ -1237,12 +1239,12 @@ isGenerativeTyCon = isInjectiveTyCon
-- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
-- with respect to representational equality?
isDistinctAlgRhs :: AlgTyConRhs -> Bool
isDistinctAlgRhs (TupleTyCon {}) = True
isDistinctAlgRhs (DataTyCon {}) = True
isDistinctAlgRhs (DataFamilyTyCon {}) = False
isDistinctAlgRhs (AbstractTyCon distinct) = distinct
isDistinctAlgRhs (NewTyCon {}) = False
isGenInjAlgRhs :: AlgTyConRhs -> Bool
isGenInjAlgRhs (TupleTyCon {}) = True
isGenInjAlgRhs (DataTyCon {}) = True
isGenInjAlgRhs (DataFamilyTyCon {}) = False
isGenInjAlgRhs (AbstractTyCon distinct) = distinct
isGenInjAlgRhs (NewTyCon {}) = False
-- | Is this 'TyCon' that for a @newtype@
isNewTyCon :: TyCon -> Bool
......@@ -1332,6 +1334,8 @@ isTypeSynonymTyCon _ = False
mightBeUnsaturatedTyCon :: TyCon -> Bool
-- True iff we can decompose (T a b c) into ((T a b) c)
-- I.e. is it injective and generative w.r.t nominal equality?
-- That is, if (T a b) ~N d e f, is it always the case that
-- (T ~N d), (a ~N e) and (b ~N f)?
-- Specifically NOT true of synonyms (open and otherwise)
--
-- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment