Too many different hashes for variations of a term?

[mitchellwrosen]

~I'm not sure if there's a bug here, but it would be good to capture this information in a transcript test (or confirm that we already have one).~ Wait, read on, I think there's definitely at least one bug lurking.

Here are a bunch of similar ways to ascribe a type to a suspended a term (in this example, foo = '175). Each group corresponds to a term with a different hash.

Group 1

User-written signature	Pretty-printed type
(No explicit type signature)	'Nat
a ->{} Nat	'Nat

Group 2

User-written signature	Pretty-printed type
'Nat	'Nat
() -> Nat	'Nat
() ->{} Nat	'Nat

Group 3

User-written signature	Pretty-printed type
() ->{e} Nat	'Nat

Group 4

User-written signature	Pretty-printed type
() ->{e1,e2} Nat	'Nat

Group 5	User-written signature	Pretty-printed type
a -> Nat	a -> Nat
a ->{e} Nat	a -> Nat

Group 6	User-written signature	Pretty-printed type
a ->{e1,e2} Nat	a -> Nat

And a couple thoughts:

• Group 4 and Group 6 essentially demonstrate the same thing: that an ability set {e1,e2} is not considered the same as {e}. On one hand, this probably does make sense, but without something like TypeApplications I'm not sure how a user would distinguish one from the other. However, we pretty-print both as 'Nat, so I think we should either normalize before hashing, or else not hide the difference when pretty-printing.

• It seems inconsistent to me that Group 2 demonstrates an unadorned arrow -> is equivalent to the empty set of abilities ->{}, whereas Group 5 demonstrates that an unadorned arrow -> is equivalent to a singleton set of abilities that contains a type var ->{e}. Am I reading that right? :thinking:

• It's surprising to me that we infer the type a ->{} Nat for the term foo = '175, but then show that type signature as 'Nat, because if you had written the type signature yourself as 'Nat, it'd be equivalent to the type signatures () -> Nat / () ->{} Nat, not a ->{} Nat. This inconsistency means a user can edit a term whose type was originally inferred (such as foo = '175), but then be told that the term is ready to be updated, not that it already exists (because it's pretty-printed with a different type 'Nat!)

• Maybe more but my brain stopped working

[mitchellwrosen]

cc @dolio, just want to make sure this is on your radar, if it seems relevant to you :stuck_out_tongue:

[dolio]

Which part is the buggy seeming part?

A lot of this is the pretty printer hiding information. I think there's a way to get it to print the exact type, but I don't recall what it is.

Adding ability variables to 'positive' ability lists gives equivalent types, and the pretty printer leaves those out. It also leaves out such ability lists entirely when they're equivalent to empty lists, because those are considered analogous to "pure" functions. In the one direction:

a ->{} b ==> forall e1 e2 e3 ... . a ->{e1,e2,e3...} b

because you can always add redundant abilities that the function doesn't really require. In the opposite direction, you can just instantiate all those variables to {}. The quantification ensures the function doesn't really use them, essentially.

It is unfortunate that these all yield different hashes. I think there's some tension with trying to canonicalize the types that people explicitly write, though. Maybe that isn't that important, though, because the pretty printer already shows a different type than the one you explicitly give in these cases.