[Haskell-cafe] Applying a Constraint to a Proxy'd type

[Ivan Lazar Miljenovic]

I'm not sure if it's possible (and I have an alternate method of doing
this so it isn't strictly speaking _necessary_, but would make the
code cleaner if I can), but I would like to convert a "value" of kind
(k -> Constraint) into one of kind (Proxy k -> Constraint).

I can achieve this using a type family (note: I've also made this
polymorphic in terms of the Proxy type used, but that isn't
necessary):

> type family LiftConstraint_ c pa :: Constraint where
>   LiftConstraint_ c (proxy a) = c a
>   LiftConstraint_ c pa        = () ~ Bool -- A nonsensical failing Constraint value

which has the problem that it can't be partially applied (which I also
need).  This can be wrapped up in a typeclass:

> class (LiftConstraint_ c pa) => LiftConstraint c pa
> instance (LiftConstraint_ c pa) => LiftConstraint c pa

The problem with this is that if I try and use it somewhere that -
having already a type of kind (c :: * -> Constraint) from the
environment - that expects a function of type (forall a. (c a) => a ->
b) with a fixed "b" value, then trying to use something like this
function prevents it from working (for the purposes of argument,
assume the old specification of Num that had an Eq superclass; this is
the way I can produce the smallest example):

> fn :: forall pn. (LiftConstraint Num (Proxy n)) => Proxy n -> Bool
> fn = join (==) . asProxyTypeOf 0

The resulting error message is: "Could not deduce (a ~ Proxy n0) ..."

This occurs even if I make the type of fn polymorphic in terms of the
proxy type or if I make LiftConstraint_ specific.  Note that the error
goes away if I make the definition to be "fn = const True"; it's only
if I try and _use_ the proxy value.

I've tried defining and using an IsProxy type family + class but that
fails to the same basic problem: it can't tell that the provided value
can be pulled apart to get what's in the Proxy.

Any ideas?

-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic at gmail.com
http://IvanMiljenovic.wordpress.com