On February 10, 2015 16:28:56 Dan Doel wrote:
> Impredicativity, with regard to type theories, generally refers to types
> being able to quantify over the collection of types that they are then a
> part of. So, the judgment:
>
>     (forall (a :: *). a -> a) :: *
>
> is impredicative, because we have a type in * that quantifies over all
> types in *, which includes itself. Impredicativity in general refers to
> this sort of (mildly) self-referential definition.

Thanks Dan and David,

That was informative.  Also very interesting that ($) is a special case.  I tried this

 newtype Wrap = Wrap { extract :: forall f. Functor f => f Int }

 trip'' :: Wrap -> Wrap
 trip'' a = Wrap $ extract a

and the compiler was happy.  Wrapping ($) as ($') gave an error as you implied it would

 trip''' :: Wrap -> Wrap
 trip''' a = Wrap $' extract a
     where ($') = ($)

With regard to my earlier comment about translating the (.) version

 trip' :: Wrap -> Wrap
 trip' = Wrap . extract

to core, I can see it's actually okay.  A most you may need is a lambda to float the implicit parameters backwards

 trip' :: Wrap -> Wrap
 trip' = Wrap . (\a f fDict -> extract f fDict a)

as GHC seems to always float them as far leftward as possible

 extract :: Functor f => Wrap -> f Int

I take it there are no user supplied types a person can give to overcome the predicative assumption?

Out of curiosity, how would you write the special internal type that ($) has that separates it from ($') above?

Thanks!  -Tyson