<p dir="ltr">See <a href="https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/">https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/</a> for some discussion. A type family application is stuck if it can't reduce further and has not reached a proper type. Given the aforementioned type family Foo, the application Foo 'False is stuck. It's a type of kind *, and it's uninhabited (but not as nicely uninhabited as Void--it offers no ex falso). This actually turns out to be useful for some things. GHC offers</p>
<p dir="ltr">type family Any :: k where {}</p>
<p dir="ltr">which is, at least,</p>
<p dir="ltr">1. A safe intermediate target for unsafeCoerce<br>
2. An utterly unsatisfiable  constraint (see the definition of Bottom in the GitHub master of the reflection package)</p>
<p dir="ltr">But sometimes you want to know something's *not* a stuck type family. See the issue I filed earlier today at <a href="https://github.com/kwf/ComonadSheet/issues/6">https://github.com/kwf/ComonadSheet/issues/6</a> for an example--the code tries to make a certain instance impossible to produce, but the possibility of stuckness defeats it as its currently written.</p>
<div class="gmail_quote">On Jan 25, 2016 1:01 AM, "Jeffrey Brown" <<a href="mailto:jeffbrown.the@gmail.com">jeffbrown.the@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">"Stuck type" is proving difficult to Google. Do you recommend any references?</div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 24, 2016 at 1:24 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Since type families can be stuck, it's sometimes useful to restrict<br>
things to sane types. At present, the most convenient way I can see to<br>
do this in general is with Typeable:<br>
<br>
type family Foo x where<br>
  Foo 'True = Int<br>
<br>
class Typeable (Foo x) => Bar x where<br>
  blah :: proxy x -> Foo x<br>
<br>
This will prevent anyone from producing the bogus instance<br>
<br>
instance Bar 'False where<br>
  blah _ = undefined<br>
<br>
Unfortunately, the Typeable constraint carries runtime overhead. One<br>
possible way around this, I think, is with a class that does just<br>
sanity checking and nothing more:<br>
<br>
class Sane (a :: k)<br>
instance Sane Int<br>
instance Sane Char<br>
instance Sane 'False<br>
instance Sane 'True<br>
instance Sane '[]<br>
instance Sane '(:)<br>
instance Sane (->)<br>
instance Sane 'Just<br>
instance Sane 'Nothing<br>
instance (Sane f, Sane x) => Sane (f x)<br>
<br>
To really do its job properly, Sane would need to have instances for<br>
all sane types and no more. An example of an insane instance of Sane<br>
would be<br>
<br>
instance Sane (a :: MyKind)<br>
<br>
which would include stuck types of kind MyKind.<br>
<br>
Would it be useful to add such an automatic-only class to GHC?<br>
<br>
David<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div><div dir="ltr">Jeffrey Benjamin Brown</div></div>
</div>
</blockquote></div>