Better type synonym merging/subtyping for Backpack
Here are two signatures which don't merge today in Backpack:
signature A where
data T
data U = Mk T
signature A where
data S
data U = Mk S
On the one hand, this is not too surprising, because you never said that T and S were the same, so why should I decide that the declarations of U are compatible? OK, but suppose I were to add the missing type synonym: which direction should I put it? What you will find is that, under Backpack's current subtyping rules, *neither* orientation is a subtype of the other:
signature A where
data T
type S = T
data U = Mk T
signature A where
type T = S
data S
data U = Mk S
The first signature is a supertype of a module that says data T = MkCommon
, but NOT of a module that says data S = MkCommon
, since type synonym declarations and data declarations are not compatible.
This doesn't smell very good. Indeed, ML's semantic signatures do not have this problem, because when I write these signatures, I actually get a semantic signature of the form exists c. { type T = c, type S = c, ... }
; i.e., neither declaration is privileged.
On the other hand, our behavior is inline with MixML, which does not have these as mutual subtypes. So it's not clear the complexity of changing our internal language justifies the marginal benefit that is to be gotten here. Not planning on fixing this unless someone shouts.
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | low |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |