GHC: Ticket #7186: problems with typelits and typenats
http://ghc.haskell.org/trac/ghc/ticket/7186
<p>
in this test case
<a class="ext-link" href="https://gist.github.com/3445419"><span class="icon"></span>https://gist.github.com/3445419</a>
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
</p>
<p>
likewise in
<a class="ext-link" href="https://gist.github.com/3445456"><span class="icon"></span>https://gist.github.com/3445456</a>
the type checker can't seem to deduce that 1<=2
which should be "trivial" :)
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7186
Trac 1.0.7carterFri, 24 Aug 2012 16:49:37 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/7186
http://ghc.haskell.org/trac/ghc/ticket/7186
<ul>
<li><strong>attachment</strong>
set to <em>gistfile1.hs</em>
</li>
</ul>
<p>
concrete inequality problem (1<=1)
</p>
TicketcarterFri, 24 Aug 2012 16:50:20 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/7186
http://ghc.haskell.org/trac/ghc/ticket/7186
<ul>
<li><strong>attachment</strong>
set to <em>gistfile1.2.hs</em>
</li>
</ul>
<p>
SingI arity problem example
</p>
TicketsimonpjMon, 27 Aug 2012 08:51:16 GMTcc, difficulty set
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:1
<ul>
<li><strong>cc</strong>
<em>iavor.diatchki@…</em> added
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Iavor, could you respond? (I've added you in cc in case you missed it.)
</p>
<p>
I think the explanation is that in 7.6 there is no useful reasoning ability (beyond equality) in nats; Iavor is working on that.
</p>
<p>
Simon
</p>
TicketiglooSat, 20 Oct 2012 20:56:36 GMTcomponent changed; milestone set
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:2
<ul>
<li><strong>component</strong>
changed from <em>Compiler</em> to <em>Compiler (Type checker)</em>
</li>
<li><strong>milestone</strong>
set to <em>7.8.1</em>
</li>
</ul>
TicketdiatchkiTue, 30 Oct 2012 17:38:43 GMT
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:3
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:3
<p>
Hello,
</p>
<p>
the reason <tt>SingI</tt> appears to have two parameters in type errors is that it is <em>kind polymorphic</em>---the first (unexpected) parameter is the kind at which the constraint was instantiated. So when you see <tt>SingI Nat d</tt>, this means that GHC could not solve the constraint <tt>SingI d</tt> (and, by the way, <tt>SingI</tt> was instantiated at kind <tt>Nat</tt>). 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.
</p>
<p>
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:
</p>
<pre class="wiki">SingI (d :: Nat)
</pre><p>
This seems nicer, and I can imagine it working well for other polymorphic types/constraints also.
</p>
<p>
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 <tt>type-nats</tt> branch of GHC.
</p>
TicketmonoidalMon, 16 Sep 2013 08:23:46 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:4
http://ghc.haskell.org/trac/ghc/ticket/7186#comment:4
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
With new type-level naturals 1<=2 example compiles in HEAD. The second problem, displaying kind variables, is covered by <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8084" title="bug: Enabling PolyKinds makes some type errors weird (closed: fixed)">#8084</a> so I'll close this ticket.
</p>
Ticket