<div dir="ltr"><div><div><div><div><div><div><div><div>Hi Ivan,<br><br></div>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<br><br>> (LiftConstraint * * EqNum (Proxy k n))<br><br></div>but if you look at the kind of LiftConstraint:<br><br>> LiftConstraint :: (k1 -> Constraint) -> k2 -> Constraint<br><br></div><div>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_.<br></div><br>One solution is to restrict the kind of what's inside the Proxy, say by adding (n :: *) in the type signature for fn.<br></div><br><br>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:<br><br></div><div>> fn :: LiftConstraint Num n => Proxy n -> Bool<br><br></div><div>But then LiftConstraint_ can't have it's second equation.<br></div><div><br><br></div><div>I think your problem comes up with a smaller type function:<br></div><div><br></div><div>> type family UnProxy x :: k where UnProxy (Proxy x) = x<br><br></div><div>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:<br><br></div><div>> type BadId x = UnProxy (Proxy x)<br></div><div>> type SillyId (x :: k) = UnProxy (Proxy x) :: k<br></div><div><br></div><div>Hope this helps.<br></div><div><br></div><div>Regards,<br></div><div>Adam<br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, May 8, 2016 at 8:15 AM, Ivan Lazar Miljenovic <span dir="ltr"><<a href="mailto:ivan.miljenovic@gmail.com" target="_blank">ivan.miljenovic@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm not sure if it's possible (and I have an alternate method of doing<br>
this so it isn't strictly speaking _necessary_, but would make the<br>
code cleaner if I can), but I would like to convert a "value" of kind<br>
(k -> Constraint) into one of kind (Proxy k -> Constraint).<br>
<br>
I can achieve this using a type family (note: I've also made this<br>
polymorphic in terms of the Proxy type used, but that isn't<br>
necessary):<br>
<br>
> type family LiftConstraint_ c pa :: Constraint where<br>
>   LiftConstraint_ c (proxy a) = c a<br>
>   LiftConstraint_ c pa        = () ~ Bool -- A nonsensical failing Constraint value<br>
<br>
which has the problem that it can't be partially applied (which I also<br>
need).  This can be wrapped up in a typeclass:<br>
<br>
> class (LiftConstraint_ c pa) => LiftConstraint c pa<br>
> instance (LiftConstraint_ c pa) => LiftConstraint c pa<br>
<br>
The problem with this is that if I try and use it somewhere that -<br>
having already a type of kind (c :: * -> Constraint) from the<br>
environment - that expects a function of type (forall a. (c a) => a -><br>
b) with a fixed "b" value, then trying to use something like this<br>
function prevents it from working (for the purposes of argument,<br>
assume the old specification of Num that had an Eq superclass; this is<br>
the way I can produce the smallest example):<br>
<br>
> fn :: forall pn. (LiftConstraint Num (Proxy n)) => Proxy n -> Bool<br>
> fn = join (==) . asProxyTypeOf 0<br>
<br>
The resulting error message is: "Could not deduce (a ~ Proxy n0) ..."<br>
<br>
This occurs even if I make the type of fn polymorphic in terms of the<br>
proxy type or if I make LiftConstraint_ specific.  Note that the error<br>
goes away if I make the definition to be "fn = const True"; it's only<br>
if I try and _use_ the proxy value.<br>
<br>
I've tried defining and using an IsProxy type family + class but that<br>
fails to the same basic problem: it can't tell that the provided value<br>
can be pulled apart to get what's in the Proxy.<br>
<br>
Any ideas?<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Ivan Lazar Miljenovic<br>
<a href="mailto:Ivan.Miljenovic@gmail.com">Ivan.Miljenovic@gmail.com</a><br>
<a href="http://IvanMiljenovic.wordpress.com" rel="noreferrer" target="_blank">http://IvanMiljenovic.wordpress.com</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</font></span></blockquote></div><br></div>