Instance name generation needs more data

[sweirich]

See base-test/NestTup.hs

Also, Data.Semigroup declares instances for both "Semigroup.First" and "Moniod.First". These two have the same name so it fails.

[nomeata]

Also, Data.Semigroup declares instances for both "Semigroup.First" and "Moniod.First". These two have the same name so it fails.

That’s on me; I removed the module name qualification in the interest of shorter instance names (since these show up in proofs). I'd like to keep that in general, so that smells like we need an edit. Or maybe detect this situation. Not sure yet.

[nomeata]

See base-test/NestTup.hs

There the code is confused that we have multiple instances with the same outermost tycon. With Haskell98 classes, that should be unique, but our “encoding” of nested tuples is not Haskell98. So the code that comes up with the name should just detect nested tuples.

[sweirich]

The issue with the two Firsts seems unlikely to be a common headache. I'd prefer to keep the names shorter and simpler. (And I don't want to modify all of our existing edit files if we change the naming scheme.)

[sweirich]

There are two things going on with Tuples --- first the instance name doesn't record more than the top level type structure. Maybe it should, as we may find more and more non-Haskell 98 out there.

The other issue is that our type mapping is not injective. We compile (a,b,c) and (a,(b,c)) to the same Coq type (a (b c)). We should update base/GHC/Tuple.v so that we can distinguish triples from these nestings.

[nomeata]

There are two things going on with Tuples --- first the instance name doesn't record more than the top level type structure. Maybe it should, as we may find more and more non-Haskell 98 out there.

GHC uses only Haskel98… but I guess we could come up with a fun naming scheme that yields the existing output for Haskell98, but distinguishes non-Haskell98 instances properly, without being too long.

The other issue is that our type mapping is not injective. We compile (a,b,c) and (a,(b,c)) to the same Coq type (a (b c)). We should update base/GHC/Tuple.v so that we can distinguish triples from these nestings.

How is that an issue? Because of overlapping instances?

What is a better type target? Can we define

Definition nTuple : nat -> Type

and map (a,b,c) to nTuple 3 a b c?

[sweirich]

Yes --- I'm worried that Haskell code could want to define one instance for (a, (b,c)) and a different instance for (a,b,c). But in Coq, we would only be able to support one of the two instances if these are the same types.

I'm actually thinking of a "worse" solution:

Inductive Tup3 (a : Type) (b : Type) (c : Type) : Type :=
   | tup3 :  a -> b -> c -> Tup a b c.

and Tup4, Tup5, etc.

[nomeata]

I came up with a nifty encoding scheme for the instance names… stay tuned.

[sweirich]

Um... this is not really a blocking problem (compared to say, inner recursion/mutual recursion). Just made an issue so we wouldn't forget.

[nomeata]

All fixed. The instance name is now the list of all type constructors (in breadth-first order), followed by a number that (together with the fixed arity of the type constructors) encodes that shape of the tree. The number is omitted if it is smallest number possible for that tree, which means that these numbers show up almost never (never with Haskell98).

This changes almost none of our instance names, only the URec instances names now (rightly) include the arguments of URec.

[nomeata]

Um... this is not really a blocking problem (compared to say, inner recursion/mutual recursion). Just made an issue so we wouldn't forget.

Some problems are more fun than others :-)

[sweirich]

Some problems are more fun than others :-)

This statement explains all commits that I make to this repo. :-)