Opened 11 months ago

Last modified 11 months ago

#13151 new task

Make all never-exported IfaceDecls implicit

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

Description

Consider the representation of an instance in an interface file. It is always associated with a DFun, but the DFun is stored as a separate IfaceDecl.

You might wonder if it's possible for an IfaceClsInst to refer to an externally defined DFun, or if it's possible to have a DFun but no IfaceClsInst associated with it. The current ClsInst representation won't tell you, but in fact, it's impossible. For example, DFuns are manually added to the type environment by TidyPgm, which literally goes through the list of ClsInsts to pull out the set of DFunIds which need to be added to the TypeEnv.

This all seems horribly indirect. Why not just *embed* the IfaceDecl describing the DFun inside IfaceClsInst, and treat the DFun as an "implicit TyThing"? This makes it clear that the instance declaration canonically defines the DFun.

To do this, we have to expand our idea of implicit TyThings; at the moment, only a TyThing can be associated with implicit TyThings. With this change, instances and family instances can also be associated with implicit TyThings. But this doesn't seem like too much.

Why does this matter? I was cleaning up some code in Backpack, and I noticed that I had written some very complicated things to handle DFuns and coercion axioms, because they were indirected through a Name, even though morally they should have been "implicit"-like things. The proposed refactor here would solve this correctness problem.

Change History (3)

comment:1 Changed 11 months ago by simonpj

I like it the way it is. Here's why.

Unfoldings for any old function might mention $fEqList the DFun for equality on lists. So there must be a top-level declaration for $fEqList in the interface file

$fEqList :: forall a. Eq a -> Eq [a]
-- ...together with arity, unfolding, strictness, whatever, just
-- like any other Id...

or at least it is simple and convenient for that to be the case. It's particularly important that it has an unfolding;l this unfolding is always a DFunUnfolding.

And once we have that, it seems simpler to refer to it from the instance decl rather than to duplicate it.

I suppose you could put all this in the instance decl. But would need to define the top-level Id $fEqList.

I have not yet grokked what's hard about the sataus quo. I'm not fundamentally against refactoring it though.

comment:2 Changed 11 months ago by ezyang

I suppose you could put all this in the instance decl. But would need to define the top-level Id $fEqList.

Yes, that's the idea. The upshot is that IfaceClsInst, which doesn't itself define any TyThings, can define an implicit TyThing, $fEqList. I agree that we still need a TyThing for $fEqList, but there isn't any reason $fEqList needs to live in mi_decls; we just have to make sure it gets to the type environment in the end.

Today, if I'm looking for an OccName from an interface, it may either be defined directly by an entry in mi_decls, or it is one of the implicit things defined by one of the IfaceDecl. My suggestion is to expand this to also include implicit things defined by IfaceClsInsts.

I have not yet grokked what's hard about the status quo.

So, the problem is more pronounced for closed type families, so I'll do an example involving them. Suppose we have a signature that looks like this:

signature A where
type family F a where
  F a = Int

This will give us a type family, which refers to an axiom TFCo:R:F that specifies F a ~ Int. Furthermore, let's suppose that we're trying to match this against the following module:

module A where
type family F a where
  F a = Bool

When we typecheck the interface to make the TyThings for the type family we are going to compare, we need to need to resolve the Name TFCo:R:F from the hsig's interface to an actual Coercion.

If we resolve TFCo:R:F to point to the *module*'s coercion, that's a disaster, because we never actually check that the top-level *coercions* match, we only check that the Coercion recorded in the type family (which we pointed at the module) matches.

"Now," you might say, "why didn't you just have TFCo:R:F point to the hsig's version, then there's no problem." This is true, but in other cases, pointing to the module's versions of TyThings is very useful. Consider this other case:

signature M where
  data T
  f :: T

module M where
  type T = Int
  f :: Int

If the T in f :: T is not resolved to type T = Int, we will conclude that f :: T and f :: Int are incompatible, when they should be compatible! I'd quite like this to work: it's very important when implementing abstract data with type synonyms.

The current implementation does a delicate tight-rope walk, of resolving names to the module version, except in the few cases where we need to resolve it to the hsig version. Highly delicate. Why does making the coercion *implicit* simplify things? With an implicit TyThing, we can avoid doing a lookup for the coercion at all; just use the implicit copy that was embedded. This means we sidestep the possible bug.

We don't have to do this refactor: maybe the more complex interface typechecking for general users outweighs the simplification in the Backpack case. But I wanted to put this proposal out there.

comment:3 Changed 11 months ago by simonpj

maybe the more complex interface typechecking for general users

I don't think it'd be much more complex. If you want to pursue this, it's ok with me. We'll see if the code looks more horrible; it'll probably be fine.

Note: See TracTickets for help on using tickets.