Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in / Register
Toggle navigation
Menu
Open sidebar
Alex D
GHC
Commits
daf1eee4
Commit
daf1eee4
authored
Jun 16, 2015
by
eir@cis.upenn.edu
Browse files
Clarify some comments around injectivity.
parent
a6b8b9c2
Changes
3
Hide whitespace changes
Inline
Sidebyside
compiler/typecheck/TcCanonical.hs
View file @
daf1eee4
...
...
@@ 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.
...
...
compiler/typecheck/TcRnDriver.hs
View file @
daf1eee4
...
...
@@ 996,7 +996,7 @@ checkBootTyCon tc1 tc2
quotes
(
text
"representational"
)
<+>
text
"in boot files."
)
eqAlgRhs
tc
(
AbstractTyCon
dis1
)
rhs2

dis1
=
check
(
is
Distinct
AlgRhs
rhs2
)
Check compatibility

dis1
=
check
(
is
GenInj
AlgRhs
rhs2
)
Check compatibility
(
text
"The natures of the declarations for"
<+>
quotes
(
ppr
tc
)
<+>
text
"are different"
)

otherwise
=
checkSuccess
...
...
compiler/types/TyCon.hs
View file @
daf1eee4
...
...
@@ 49,7 +49,7 @@ module TyCon(
isOpenTypeFamilyTyCon
,
isClosedSynFamilyTyConWithAxiom_maybe
,
isBuiltInSynFamTyCon_maybe
,
isUnLiftedTyCon
,
isGadtSyntaxTyCon
,
isInjectiveTyCon
,
isGenerativeTyCon
,
is
Distinct
AlgRhs
,
isGadtSyntaxTyCon
,
isInjectiveTyCon
,
isGenerativeTyCon
,
is
GenInj
AlgRhs
,
isTyConAssoc
,
tyConAssoc_maybe
,
isRecursiveTyCon
,
isImplicitTyCon
,
...
...
@@ 1165,7 +1165,7 @@ isAbstractTyCon _ = False
 algebraic
makeTyConAbstract
::
TyCon
>
TyCon
makeTyConAbstract
tc
@
(
AlgTyCon
{
algTcRhs
=
rhs
})
=
tc
{
algTcRhs
=
AbstractTyCon
(
is
Distinct
AlgRhs
rhs
)
}
=
tc
{
algTcRhs
=
AbstractTyCon
(
is
GenInj
AlgRhs
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
=
is
Distinct
AlgRhs
rhs
=
is
GenInj
AlgRhs
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?
is
Distinct
AlgRhs
::
AlgTyConRhs
>
Bool
is
Distinct
AlgRhs
(
TupleTyCon
{})
=
True
is
Distinct
AlgRhs
(
DataTyCon
{})
=
True
is
Distinct
AlgRhs
(
DataFamilyTyCon
{})
=
False
is
Distinct
AlgRhs
(
AbstractTyCon
distinct
)
=
distinct
is
Distinct
AlgRhs
(
NewTyCon
{})
=
False
is
GenInj
AlgRhs
::
AlgTyConRhs
>
Bool
is
GenInj
AlgRhs
(
TupleTyCon
{})
=
True
is
GenInj
AlgRhs
(
DataTyCon
{})
=
True
is
GenInj
AlgRhs
(
DataFamilyTyCon
{})
=
False
is
GenInj
AlgRhs
(
AbstractTyCon
distinct
)
=
distinct
is
GenInj
AlgRhs
(
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
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment