Do singled case expressions need an explicit kind annotation?

[RyanGlScott]

While pursuing a fix for #542, I uncovered this interesting piece of code:

singletons/singletons-th/src/Data/Singletons/TH/Single.hs

Lines 959 to 965 in c419ece

	singExp (ADCaseE exp matches ret_ty) res_ki =
	-- See Note [Annotate case return type] and
	-- Note [The id hack; or, how singletons-th learned to stop worrying and
	-- avoid kind generalization]
	DAppE (DAppTypeE (DVarE 'id)
	(singFamily `DAppT` (ret_ty `maybeSigT` res_ki)))
	<$> (DCaseE <$> singExp exp Nothing <*> mapM (singMatch res_ki) matches)

In particular, the part of interest is the ret_ty `maybeSigT` res_ki bit. Why do we need the explicit res_ki kind annotation? That is, why do we need id @(Sing (t :: k)) e instead of just id @(Sing t) e? This is what Note [Annotate case return type] has to say:

singletons/singletons-th/src/Data/Singletons/TH/Single.hs

Lines 824 to 837 in c419ece

	-- Note [Annotate case return type]
	-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	--
	-- We're straining GHC's type inference here. One particular trouble area
	-- is determining the return type of a GADT pattern match. In general, GHC
	-- cannot infer return types of GADT pattern matches because the return type
	-- becomes "untouchable" in the case matches. See the OutsideIn paper. But,
	-- during singletonization, we *know* the return type. So, just add a type
	-- annotation. See #54.
	--
	-- In particular, we add a type annotation in a somewhat unorthodox fashion.
	-- Instead of the usual `(x :: t)`, we use `id @t x`. See
	-- Note [The id hack; or, how singletons-th learned to stop worrying and avoid
	-- kind generalization] for an explanation of why we do this.

Curiously, this Note never actually discusses the kind annotation portion of the code. As an experiment, I decided to change ret_ty `maybeSigT` res_ki in the code to just ret_ty, and everything in singletons-base and its test suite continued to compile.

As historical context, this kind annotation was added in a60b000 in pursuit of a fix for #136. It's possible that this kind annotation was needed at the time, especially since case expressions were singled as e :: Sing (t :: k) rather than id @(Sing (t :: k)) e. This is because former interacts with kind generalization differently than the latter—see Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization] for the details. Now that singletons-th uses the id hack, it's quite possible that the kind annotation is no longer required due to the lack of kind generalization.

[RyanGlScott]

For some additional background on why I am interested in removing this kind annotation, consider this example:

absurd :: forall a. Void -> a
absurd v = case v of {}

Currently, this singles to something resembling:

sAbsurd :: forall a (v :: Void). Sing v -> Sing (Absurd v :: a)
sAbsurd (sV :: Sing v) = id @(Sing (Case v :: a)) (case sV of {})

Crucially, sAbsurd relies on a being in scope in id @(Sing (Case v :: a)). This is made possibly by a being quantified by an outermost forall. Without the outermost forall, GHC would reject sAbsurd.

Now consider what would happen in a variant of absurd that uses a nested forall:

absurd' :: Void -> forall a. a
absurd' v = case v of {}

If we singled absurd' naïvely using the approach outlined in #542, we'd get:

sAbsurd' :: forall (v :: Void). Sing v -> forall a. Sing (Absurd' v :: a)
sAbsurd' (sV :: Sing v) = id @(Sing (Case v :: a)) (case sV of {})

Unfortunately, this is not well scoped. Since the forall a. is not an outermost forall, the a in id @(Sing (Case v :: a)) is not in scope.

Possible ways to fix this include:

1. Move the forall a to be on the outside in the type of sAbsurd'. While possible, I'd be sad to pick this option, as it would mean that the order of foralls would be substantially different between absurd' and sAbsurd'.

2. Use the following trick to bring a into scope in the body of sAbsurd':

   sAbsurd' :: forall (v :: Void). Sing v -> forall a. Sing (Absurd' v :: a)
   sAbsurd' (sV :: Sing v) =
     (id @(Sing (Case v :: a)) (case sV of {}))
       :: forall a. Sing (Absurd' v :: a)

   This works, but figuring out how to generate this code automatically would be a bit tricky. In particular, we'd have to figure out which type variables to quantify. (Note that we wrote forall a. and not forall a v..)

3. Remove the kind annotation entirely as described in the comment above. That way, a will never appear in the body of the function to begin with, which avoids the problem entirely. This seems like the simplest solution, so I'm inclined to go with this one unless there is some unforeseen difficulty with it.