UlfNorell
commented
10 years ago From andreas....@gmail.com on November 11, 2013 14:19:57
That reminds me of a paper of Randy Pollack I have read 13 years ago. Quoting from "Dependently Typed Records", beginning of Section 3.3:
Labels and Variables. Labels are the global accessors for records, and hence cannot be alpha converted. Thus labels and variables cannot be the same syntactic class in dependent record types, or else how could we substitute y for x in y: Set, z: x . To my knowledge, the first satisfactory handling of this problem is in [HL94], where every field has both a label (that does not bind) and a variable (that does bind). PER would be written as {S ⊲ s:Set, R ⊲ r :(s)(s)Prop, sAx ⊲ :sym(s)(r), tAx ⊲ :trn(s)(r) }.
In our terms, this would mean that we should print the scrutinee as:
{A = A1 : Set} -> A1 -> A1
and maybe also parse such beasts!?
From andreas....@gmail.com on November 11, 2013 23:03:02
Here is another issue with printing hidden function types (see also issue 951 ):
postulate f : {A : Set₁} → A → A
module _ (A : Set) where
test : Set → Set test = f {A₁ = Set}
-- Bad printing of hidden function type in error:
-- Function does not accept argument {A₁ = _} -- when checking that {A₁ = Set} are valid arguments to a function of -- type {A₁ : Set₁} → A₁ → A₁
Names of hidden arguments are not subject to alpha-equality!
Thus, when we put (A : Set) into the context, we cannot print the type of f as {A₁ : Set₁} → A₁ → A₁, because that suggests that the argument it expects has name A₁. We rather have to choose a different name for the variable A bound in context, in case it should be printed as well.
Original issue: http://code.google.com/p/agda/issues/detail?id=952