type error messages contains weired characters

Stream: new members

[Xipan Xiao]

I have some code like:

apply IsLocalization.map_units' A (Localization S) s

Where A is a commutative ring and S is multiplicative set (submonoid). And the error message says

application type mismatch
  IsLocalization.map_units' A
argument
  A
has type
  Type u_1 : Type (u_1 + 1)
but is expected to have type
  ↥?m.10254 : Type ?u.10251

I know I'm not providing the parameters correctly, but how do I know which type it expects if it shows something like ↥?m.10254 : Type ?u.10251? Is it always like this, or is it because my installation is incomplete or misconfigured?

[Aaron Liu]

You should use the unprimed version

[Aaron Liu]

you can usually get the type information with a mouse hover or looking at the infoview, but if that doesn't work you can go to the #docs

[Robert Maxton]

Also, for the record, ?m.10254 is a metavariable, and ?u.10251 is a universe level metavariable. They stand for types or levels that the compiler hasn't figured out how to solve for yet; when they show up in type errors, they indicate that the compiler has incomplete information about the expected type (insufficient information to pin down the exact type), but what it has already conflicts with what you've given.

[Aaron Liu]

Robert Maxton said:

They stand for types or levels that the compiler hasn't figured out how to solve for yet;

it's actually the elaborator that fills in the holes, the compiler is the thing that generates executable code from a complete definition