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 Rev(s): | ||
Wiki Page: |
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)
Change History (6)
Changed 3 years ago by carter
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.
concrete inequality problem (1<=1)