Opened 4 weeks ago

#13361 new bug

Better type synonym merging/subtyping for Backpack

Reported by: ezyang Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: backpack Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (0)

Note: See TracTickets for help on using tickets.