GitLab

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