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