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

Hi Adam, On 9 May 2016 at 07:15, adam vogt wrote:

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 forgot to mention in my simplified example that I was already doing that.

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.

The problem for me is that this makes my more general "take an arbitrary `a' that satisfies the constraint" approach. I'm beginning to think that this isn't possible; specifically because there's no way for GHC to infer that _only_ values of the form (Proxy a) can satisfy the constraint as I can't put the Proxy usage into the typeclass. So it looks like I have to try and generalise my function even more.

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.

Well, it helps me work out that my approach is almost definitely wrong, but I suppose that's better than continually bashing my head at it :p

Regards, Adam

On Sun, May 8, 2016 at 8:15 AM, Ivan Lazar Miljenovic 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@gmail.com http://IvanMiljenovic.wordpress.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

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