#7186: problems with typelits and typenats
----------------------------------------+-----------------------------------
Reporter: carter | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 7.8.1
Component: Compiler (Type checker) | Version: 7.6.1-rc1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Comment(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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7186#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
