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

[adam vogt]

Hi Ivan,

When I compile your file with -fprint-explicit-kinds (which is very helpful
to make sense of code using -XPolyKinds), the type error includes an
inferred type like

> (LiftConstraint * * EqNum (Proxy k n))

but if you look at the kind of LiftConstraint:

> LiftConstraint :: (k1 -> Constraint) -> k2 -> Constraint

You need the k1 to be equal to the k that's inside the Proxy, but ghc
decides that the k1 and k2 are * early on, and then cannot change that
decision after choosing an equation for LiftConstraint_.

One solution is to restrict the kind of what's inside the Proxy, say by
adding (n :: *) in the type signature for fn.


I think a general rule for poly-kinded proxies is that you should "pattern
match" on them in the class method signature and not in the instance heads
(or the equivalent using other language features). In your case it would
involve changing LiftConstraint etc. so that you could write:

> fn :: LiftConstraint Num n => Proxy n -> Bool

But then LiftConstraint_ can't have it's second equation.


I think your problem comes up with a smaller type function:

> type family UnProxy x :: k where UnProxy (Proxy x) = x

You could say that 'k' could be determined by what is inside Proxy. But ghc
depends on the caller of UnProxy to decide what the 'k' is and complains
when it guessed wrong instead. The type constructor Proxy is more like
Dynamic than Maybe: `(fromDynamic . toDyn) :: (Typeable a, Typeable b) => a
-> Maybe b` probably ought to have type `Typeable a => a -> Maybe a`, but
it doesn't in the same way that this fails without an additional kind
signature:

> type BadId x = UnProxy (Proxy x)
> type SillyId (x :: k) = UnProxy (Proxy x) :: k

Hope this helps.

Regards,
Adam

On Sun, May 8, 2016 at 8:15 AM, Ivan Lazar Miljenovic <
ivan.miljenovic at gmail.com> wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160508/34a1f19a/attachment.html>