@RyanGlScott Of the three bullet points you mentioned, do any correspond to making kind parameters "float"?
The result of partially applying a polykinded type constructor depends on the position of the quantifiers in the inferred or annotated kind of the type constructor.
Here is a type constructor:
data Const a b = Const a b
With XPolyKinds
enabled, here is the inferred kind of this type constructor:
Data.Functor.Const.Const :: forall k. * > k > *
Just for completeness, explicitly annotating this kind as follows makes no difference as far as the problem discussed below goes:
data Const :: forall k. * > k > *
where
Const :: a > Const a b
Here is a class:
class Something (f :: forall k. k > *)
At the term level, we expect a partial application of const :: forall x y. x > y > x
to have type const "foo" :: forall y. y > String
. Analogously, one might hope that a partial application of Const :: forall k. * > k > *
would have kind Const String :: forall k. k > *
. This would mean that the following instance declaration would be legal:
instance Something (Const String)
Alas, this does not work:
• Expected kind ‘forall k. k > *’,
but ‘Const String’ has kind ‘k0 > *’
• In the first argument of ‘Something’, namely ‘(Const String)’
In the instance declaration for ‘Something (Const String)’
If on the other hand we explicitly annotate the kind of Const
and shuffle the quantifier around:
data Const :: * > forall k. k > *
where
Const :: a > Const a b
The same instance declaration works.
This code should compile:
data Const a b = Const a b
class Something (f :: forall k. k > *)
instance Something (Const String)
Just accidentally blew up in a program because I didn't think through that maximumBy
is unsafe (it internally uses fold1
). Thankfully it was only a toy program.
Consider the following code:
{# LANGUAGE
KindSignatures
, DataKinds
, TypeFamilies
, StandaloneDeriving
, PartialTypeSignatures
, TypeFamilyDependencies
, FlexibleInstances
, FlexibleContexts
, UndecidableInstances
, TypeApplications
#}
module Main where
data Idx = Foo  Bar
type family F (a :: Idx) b where
F Foo String = Int
F Foo Int = String
F Bar String = String
F Bar Int = Int
data Test (i :: Idx) = Test { userId :: F i String, userName :: F i Int }
 deriving Show  this won't work
deriving instance
 _ =>  this won't work either
(Show (F i String), Show (F i Int)) =>  this works
Show (Test i)
main :: IO ()
main = print $ Test @Foo (1 :: Int) "foo"
(sorry if the example has a few red herrings, just translating something from slack).
You can see that the constraints in the standalone deriving declaration duplicate the fields of the Test
ADT. The compiler is actually aware of all the constraints it would need to demand in order to provide a derived instance of Show
for Test i
, it just won't go ahead and infer them.
Provide some mechanism (doesn't necessarily have to be data Test = ... deriving Show
or deriving instance _ => Show (Test i)
) that allows us to just say "yeah, about those missing constraints, just go ahead and demand them and give me an instance".
NB: The type family stuff might be a little bit of a red herring, I think the inability to derive data Test f i = Test { userId :: f i String, userName :: f i Int } deriving Show
is the same underlying issue.
Can't put a quantified constraint in a type synonym.
Put the following into a file test.hs
, then run ghci test.hs
:
{# LANGUAGE
RankNTypes,
QuantifiedConstraints,
ConstraintKinds #}
module Foo where
type Foo f = (forall s. Semigroup s => Semigroup (f s))
You get the error:
[1 of 1] Compiling Foo ( test.hs, interpreted )
test.hs:8:40: error:
• Expected a type, but ‘Semigroup (f s)’ has kind ‘Constraint’
• In the type ‘(forall s. Semigroup s => Semigroup (f s))’
In the type declaration for ‘Foo’

8  type Foo f = (forall s. Semigroup s => Semigroup (f s))
 ^^^^^^^^^^^^^^^
Failed, no modules loaded.
It should compile, and the type synonym Foo
should have kind Foo :: (* > *) > Constraint
.