Type naming doesn't propagate through records

[weaversa]

a : {myType} (fin myType) => [myType] -> { first : [myType] }
a x = { first = x }

Main> :t a
a : {myType} (fin myType) => [myType] -> {first : [myType]}
Main> :t a.first
a.first : {n} (fin n) => [n] -> [n]

[robdockins]

FWIW, similar behavior with tuples. I suspect this is down to some detail regarding how unification works in the typechecker causing a unification variable to end up with an autogenerated name.

b : {myType} (fin myType) => [myType] -> ([myType], Bit)
b x = (x, False)

Main> :t b.1
b.1 : {n} (fin n) => [n] -> Bit
Main> :t b.0
b.0 : {n} (fin n) => [n] -> [n]

[brianhuffman]

This is exactly the behavior I would expect. I'll try to explain what's happening here: Because a has a polymorphic type, when you use it in the expression a.first, the typechecker instantiates it by creating a fresh unification variable for each type argument. The type of the instantiated a is something like [?n`123] -> {first : [?n`123]}, where ?n`123 is the fresh unification variable. Projecting field first then yields type [?n`123] -> [?n`123]. Finally, the typechecker does a generalization pass, where all the remaining unification variables are turned into type parameters; for generalization, names are generated based on their kinds (preferring a, b, c, d, e for kind *, and n, m, i, j, k for kind #). (See 4c6a69c.)

I guess what you'd rather have is for the preferred name to based on the original parameter name when the polymorphic variable was instantiated. For example, the instantiated a would have had the type [?myType`123] -> {first : [?myType`123]}, and then during generalization, we would prefer the parameter name myType for the unification variable ?myType`123 instead of making a new name based on its kind.

I actually don't think it's the best idea to do this everywhere, as I think the results would often be messy and/or surprising. For example, during typechecking, two unification variables ?myType and ?yourType might be unified with each other. Which name should be used for the result? The unification algorithm might add a substitution in either direction to unify those variables, so it might be hard to predict which name would get used in the result. What would probably happen in practice is that instead of seeing mostly your own type variable names in inferred types, you'd see a bunch of names that come from type parameters of things in the Cryptol prelude. For example, if you write a polymorphic term that involves numeric literals, you'll see the names val and rep show up a lot. I'm not sure if that's really what you want.

[brianhuffman]

I don't think we're planning to do anything about this.