GHC: Ticket #15691: Marking Pred(S n) = n as injective
http://trac.haskell.org/trac/ghc/ticket/15691
<p>
Should <code>Pred</code> be injective? Please close the ticket if this is a known limitation
</p>
<div class="wikicode"><div class="code"><pre><span class="cm">{# Language DataKinds, TypeFamilyDependencies #}</span>
<span class="kr">data</span> <span class="kt">N</span> <span class="ow">=</span> <span class="kt">O</span> <span class="o"></span> <span class="kt">S</span> <span class="kt">N</span>
<span class="kr">type</span> <span class="kr">family</span>
<span class="kt">Pred</span> n <span class="ow">=</span> res <span class="o"></span> res <span class="ow">></span> n <span class="kr">where</span>
<span class="kt">Pred</span><span class="p">(</span><span class="kt">S</span> n<span class="p">)</span> <span class="ow">=</span> n
</pre></div></div><p>
fails with
</p>
<pre class="wiki"> • Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n  Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’

7  Pred(S n) = n
 ^^^^^^^^^^^^^
</pre>enusGHChttp://trac.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://trac.haskell.org/trac/ghc/ticket/15691
Trac 1.2.2monoidalSun, 30 Sep 2018 14:20:29 GMTstatus changed; cc, resolution set
http://trac.haskell.org/trac/ghc/ticket/15691#comment:1
http://trac.haskell.org/trac/ghc/ticket/15691#comment:1
<ul>
<li><strong>cc</strong>
<em>goldfire</em> added
</li>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
Yes, it's a known limitation. See <a class="extlink" href="http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peytonjones_eisenberg_injectivity.pdf"><span class="icon"></span>Injective Type Families for Haskell</a>, section 4.1, "Awkward Case 2".
</p>
<p>
By definition of <code>Pred</code> we have <code>Pred (S (Pred Zero)) ~ Pred Zero</code>. If <code>Pred</code> is recognized as injective, then <code>Zero ~ S (Pred Zero)</code>, which is a contradiction. The problem is that <code>Pred Zero</code> is a valid type, even though it's outside of the domain of <code>Pred</code>. See also <a class="new ticket" href="http://trac.haskell.org/trac/ghc/ticket/9636" title="#9636: bug: Function with type error accepted (new)">#9636</a>.
</p>
<p>
The <a class="extlink" href="https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs"><span class="icon"></span>Constrained Type Families</a> paper resolves this by representing the domain of the type function as a constraint. I don't know if there are plans to implement it.
</p>
TicketgoldfireMon, 01 Oct 2018 02:59:39 GMT
http://trac.haskell.org/trac/ghc/ticket/15691#comment:2
http://trac.haskell.org/trac/ghc/ticket/15691#comment:2
<p>
There are no current plans to implement "Constrained Type Families". The natural way to do it requires dependent types (because it requires the appearance of dictionaries, which are terms, in types). We could hack something together that didn't use dependent types, but it would be a hack.
</p>
<p>
I would love to see Constrained Type Families indeed implemented once we have dependent types.
</p>
Ticket