I’m not sure I follow. Are you expecting constrained @Int to work? You just specified that the kind has to be Type -> Type, which Int isn’t, but Maybe is. Maybe the confusion that you are referring to is the inferred kind for t in constrained. You did not specify a kind for t, but it will get elaborated to constrained :: forall (@t :: Type -> Type). Proxy t due to inference. It’s true that the compiler elaborates kinds for type variable binders, and does not require you to specify them in all cases.
Yup, if the type signature of a function is forall t. Proxy t, I expected to be able to instantiate t to anything. I guess that’s incorrect because the type ‘t’ may have inferred kind constraints.
It would be nice to force the kind if not truly polymorphic or ‘Type’, to appear in the type signature.
The compiler doesn’t do that for any other type variables though. How is the kind for t different than a kind for some m with a Monad constraint? That rule would force a lot of code to need kind signatures!
I totally get what you mean, I’m just thinking about it from the programmers perspective, and programming with types instead of having to look at the implementation.
With a class, the signature provides enough information to see how the type is constrained. For example, if a function foo has a Monad constraint, I know that I can only call it with types that have an instance of Monad. That’s the constraint and it’s specified in the signature.
I can then look at the Monad typeclass and see that the only way to implement this is for something with kind ‘Type → Type’. But that’s okay because the function ‘foo’ is not lying about it because it really only depends upon something being a Monad.
Even the class Monad is not lying about it because it effectively says that to get a Monad you only need to implement bind :: m a -> (a -> m b) -> m b and pure :: a -> m a. And it just so happens that you can only implement it for some kind of types.
Whereas a function having the type forall t. Proxy t, and not allowing all types that are allowed by Proxy seems a bit problematic to me.
Would you consider this to be weird in the same way?
data F f = Nil | Some (f Int)
empty :: forall f. F f
empty = Nil
This is constrained in the exact same way as your Proxy example, and no kind annotations in sight. That is, from the type system’s perspective, Nil and Proxy @(Type -> Type) are the same thing.
I do understand what you’re getting at, but it seems like it may only be confusing specifically because of Proxy? However, you are instantiating it with a Type -> Type kind explicitly, so I’m not entirely sure why one would expect t to accept any kind.