7

In Haskell in Depth, Chapter 11, there's an example aimed at avoiding character escaping in GHCi, which is what happens automatically when you enter print "ë", as it'll be printed like "\235" instead of "ë".

Part of the solution relies on this code:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}

data UnescapingChar = UnescapingChar { unescapingChar :: Char }

type family ToUnescapingTF (a :: k) :: k where
  {- 1 -} ToUnescapingTF Char = UnescapingChar
  {- 2 -} ToUnescapingTF (t b :: k) = (ToUnescapingTF t) (ToUnescapingTF b)
  {- 3 -} ToUnescapingTF a = a

which would fail to compile for me on line 1 with error

 • Expected kind ‘k’, but ‘Char’ has kind ‘*’
 • In the first argument of ‘ToUnescapingTF’, namely ‘Char’
   In the type family declaration for ‘ToUnescapingTF’ [GHC-25897]

and, if I comment that out, it fails on line 2 with

 • Expected kind ‘k’, but ‘t’ has kind ‘k -> k’
 • In the first argument of ‘ToUnescapingTF’, namely ‘t’
   In the type ‘(ToUnescapingTF t) (ToUnescapingTF b)’
   In the type family declaration for ‘ToUnescapingTF’ [GHC-25897]

It turns out it failed because I'm building with GHC2024, whereas the examples from the book are built with Haskell2010. Trying the extensions included in Haskell2010 one by one with my GHC2024 project, I've found I can compile if I also include CUSKs (at which point it looks like I can drop PolyKinds).

Now, I'm not sure including CUSKs is the way to go, because I read this about it:

NB! This is a legacy feature, see StandaloneKindSignatures for the modern replacement.

but StandaloneKindSignatures doesn't mention CUSKs at all, other than in saying that StandaloneKindSignatures implies NoCUSKs.

How can I go about it?

Improve this question

2 Answers 2

Reset to default
5

It seems ToUnescapingTF must preserve the kind of its type argument. And its type argument is not always Type (as in ToUnescapingTF t).

This definition with a standalone kind signature compiles for me:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

type ToUnescapingTF :: k -> k
type family ToUnescapingTF a where
  {- 1 -} ToUnescapingTF Char = UnescapingChar
  {- 2 -} ToUnescapingTF (t b) = (ToUnescapingTF t) (ToUnescapingTF b)
  {- 3 -} ToUnescapingTF a = a

I'm not sure why your example ceased to compile, however. It might be related to point #4 in this article: "SAKS make kind inference more predictable".

The approach that GHC ended up settling on was the notion of complete, user-specific kind signatures, or CUSKs for short. [...]

CUSKs are good enough for GHC, but they are endlessly confusing for users. [...] Surely there must be a better alternative to CUSKs?

The only difference is that I replaced “CUSK” with “standalone kind signature”, but this is a critical difference. GHC users have already been trained to add a signature when the type inference engine isn’t smart enough to infer a type for a value, and now the exact same training carries over to type-level declarations as well. Hooray!

enabling NoCUSKs will cause the standalone kind signature versions of Algorithms 1 and 2 to be used instead. (The StandaloneKindSignatures extension implies NoCUSKs.) A future version of GHC will likely switch the default from CUSKs to NoCUSKs.

Edit: a more detailed explanation.

ToUnescapingTF is a closed, recusive type family. And it's polymorphically recursive, in that the kind of the argument can change between invocations. Such polymorphic recursion requires extra type annotation effort when defining the type family.

Formerly (with CUSKs) these extra type annotations were given in the definition itself. The docs say that, for closed type families:

A closed type family has a complete signature when all of its type variables are annotated and a return kind (with a top-level ::) is supplied.

The definition in the book satisfies this condition, so it compiled correctly when CUSKs was on. However, CUSKs ceased to be the default at at some point, and now the extra annotation effort must go into the standalone kind signature, here type ToUnescapingTF :: k -> k. The annotations in the definition itself can still be useful, but aren't used to "choose" the correct way of typechecking of the polymorphic recursion anymore.

Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

But the type your solution is expressing is the same, right? As in, the original code's (a :: k) :: k means that ToUnescapingTF takes an a of kind k and returns a k, and the :: k -> k in your snippet is saying the same. Am I correct?
@Enlico Yes, they mean the same thing.
2

The specific issue you are running into is explained in the manual under 6.4.13.14. Kind inference in closed type families. A type family is "kind-indexed" if it requires matching on (implicit) kind variables, where it is understood that types can only be matched once their kinds are known to be matched.

Any kind-polymorphic recursive type family is necessarily kind-indexed, but there are more innocuous examples of kind-indexed type families. Given the following definitions:

type family Foo a where
    Foo Maybe = ()
    Foo [] = ()
type family Bar (a :: k) where
    Bar a = ()
type family Baaz a where
    Baaz Char = ()
    Baaz [] = ()
type family Quux (a :: k) where
    Quux Char = ()

both Foo and Bar are not kind-indexed, and both Baaz and Quux are kind-indexed.

Foo is not kind-index because its kind is Foo :: (Type -> Type) -> Type, so its argument is always known, in any well-kinded expression, to be of kind Type -> Type, so its definition need only match on a type argument. Bar is not kind-indexed because even though it can accept an argument of any kind k, there is no need to match on k to apply the definition, since Bar a = () matches an argument of any kind a :: k.

Baaz is kind-indexed because it has kind k -> Type, and we can't match the argument of kind k without first checking the kind k to see if it is Type (the Foo Char branch) or Type -> Type (the Foo [] branch). Similarly, Quux is kind-indexed because it, too, has kind k -> Type, and applying its definition requires matching the implicit kind argument k to Type before matching the explicit type argument a to Char.

As per the manual, kind-indexed type families will not have their kinds inferred unless they have a standalone kind signature or a complete user-supplied kind signature. So, the definition:

type family Quux (a :: k) where
    Quux Char = ()

does not compile because there is neither a kind signature nor a CUSK. This compiles (as long as the CUSKs extension is enabled):

{-# LANGUAGE CUSKs #-}
import Data.Kind
type family Quux (a :: k) :: Type where
--                        ^^^^^^^
    Quux Char = ()

because adding the kind annotation of the returned type makes it a CUSK, and this compiles:

import Data.Kind
type Quux :: k -> Type
type family Quux a where
    Quux Char = ()

because it has a standalone type signature.

Note that, in your example, even the simplified type:

data UnescapingChar = UnescapingChar { unescapingChar :: Char }

type family ToUnescapingTF (a :: k) :: k where
  ToUnescapingTF Char = UnescapingChar

is essentially the same as Quux. It's a kind-indexed closed type family, so it needs either the CUSKs extension or a standalone kind signature to compile.

Improve this answer

Comments

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.