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

[Ivan Lazar Miljenovic]

Hi Adam,

On 9 May 2016 at 07:15, adam vogt <vogt.adam at gmail.com> 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
> <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
>
>



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