See https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/ 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
type family Any :: k where {} which is, at least, 1. A safe intermediate target for unsafeCoerce 2. An utterly unsatisfiable constraint (see the definition of Bottom in the GitHub master of the reflection package) But sometimes you want to know something's *not* a stuck type family. See the issue I filed earlier today at https://github.com/kwf/ComonadSheet/issues/6 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. On Jan 25, 2016 1:01 AM, "Jeffrey Brown" <jeffbrown....@gmail.com> wrote: > "Stuck type" is proving difficult to Google. Do you recommend any > references? > > On Sun, Jan 24, 2016 at 1:24 PM, David Feuer <david.fe...@gmail.com> > wrote: > >> Since type families can be stuck, it's sometimes useful to restrict >> things to sane types. At present, the most convenient way I can see to >> do this in general is with Typeable: >> >> type family Foo x where >> Foo 'True = Int >> >> class Typeable (Foo x) => Bar x where >> blah :: proxy x -> Foo x >> >> This will prevent anyone from producing the bogus instance >> >> instance Bar 'False where >> blah _ = undefined >> >> Unfortunately, the Typeable constraint carries runtime overhead. One >> possible way around this, I think, is with a class that does just >> sanity checking and nothing more: >> >> class Sane (a :: k) >> instance Sane Int >> instance Sane Char >> instance Sane 'False >> instance Sane 'True >> instance Sane '[] >> instance Sane '(:) >> instance Sane (->) >> instance Sane 'Just >> instance Sane 'Nothing >> instance (Sane f, Sane x) => Sane (f x) >> >> To really do its job properly, Sane would need to have instances for >> all sane types and no more. An example of an insane instance of Sane >> would be >> >> instance Sane (a :: MyKind) >> >> which would include stuck types of kind MyKind. >> >> Would it be useful to add such an automatic-only class to GHC? >> >> David >> _______________________________________________ >> Libraries mailing list >> librar...@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> > > > > -- > Jeffrey Benjamin Brown >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs