Opened 3 years ago

Closed 2 years ago

#7186 closed bug (fixed)

problems with typelits and typenats

Reported by: carter Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.6.1-rc1
Keywords: Cc: iavor.diatchki@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

in this test case https://gist.github.com/3445419 in this case, the type errors seem to indicate SingI has two parameters, but the documentation and the error free usage both point to one parameter

likewise in https://gist.github.com/3445456 the type checker can't seem to deduce that 1<=2 which should be "trivial" :)

Attachments (2)

gistfile1.hs (1.7 KB) - added by carter 3 years ago.
concrete inequality problem (1<=1)
gistfile1.2.hs (1.8 KB) - added by carter 3 years ago.
SingI arity problem example

Download all attachments as: .zip

Change History (6)

Changed 3 years ago by carter

concrete inequality problem (1<=1)

Changed 3 years ago by carter

SingI arity problem example

comment:1 Changed 3 years ago by simonpj

  • Cc iavor.diatchki@… added
  • difficulty set to Unknown

Iavor, could you respond? (I've added you in cc in case you missed it.)

I think the explanation is that in 7.6 there is no useful reasoning ability (beyond equality) in nats; Iavor is working on that.

Simon

comment:2 Changed 3 years ago by igloo

  • Component changed from Compiler to Compiler (Type checker)
  • Milestone set to 7.8.1

comment:3 Changed 3 years ago by diatchki

Hello,

the reason SingI appears to have two parameters in type errors is that it is kind polymorphic---the first (unexpected) parameter is the kind at which the constraint was instantiated. So when you see SingI Nat d, this means that GHC could not solve the constraint SingI d (and, by the way, SingI was instantiated at kind Nat). I agree that, perhaps, this is not very obvious in the way GHC renders the type, but this is how polymorphic kinds work at the moment.

One alternative I've considered trying to implement is a rendering mode where the kinds of types are displayed, but instantiations are hidden. In this mode, the above constraint would look like this:

SingI (d :: Nat)

This seems nicer, and I can imagine it working well for other polymorphic types/constraints also.

On the second point---Simon's comment is exactly right: GHC 7.6.1 knows nothing (not even trivial facts) about the operations on type naturals. I am working on a solver, which seems to work reasonably well at the moment---if you are feeling adventures you can try it out by checking out and build the type-nats branch of GHC.

comment:4 Changed 2 years ago by monoidal

  • Resolution set to fixed
  • Status changed from new to closed

With new type-level naturals 1<=2 example compiles in HEAD. The second problem, displaying kind variables, is covered by #8084 so I'll close this ticket.

Note: See TracTickets for help on using tickets.