Why does ghci desugar type lists and type families? Can this be selectively disabled?-Collection of common programming errors

2 years ago

admin

2 minutes

I’m trying to make the types ghci displays for my libraries as intuitive as possible, but I’m running into a lot of difficulties when using more advanced type features.

Let’s say I have this code in a file:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data Container (xs::[*]) = Container

I load it up in ghci, then I type the following command:

ghci> :t undefined :: Container '[String,String,String,String,String]

Unfortunately, ghci gives me the rather ugly looking:

:: Container
       ((':)
          *
          String
          ((':)
             * String ((':) * String ((':) * String ((':) * String ('[] *))))))

ghci has removed the sugar for type level strings. Is there any way to prevent ghci from doing this and giving me just the pretty version?

On a related note, lets say I create a type level Replicate function

data Nat1 = Zero | Succ Nat1

type family Replicate (n::Nat1) x :: [*]
type instance Replicate Zero x = '[]
type instance Replicate (Succ n) x = x ': (Replicate n x)

type LotsOfStrings = Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String

Now, when I ask ghci for a type using LotsOfStrings:

ghci> :t undefined :: Container LotsOfStrings

ghci is nice and gives me the pretty result:

undefined :: Container LotsOfStrings

But if I ask for the Replicated version,

ghci> :t undefined :: Container (Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String)

ghci substitutes in for the type family when it didn’t do that for the type synonym:

:: Container
       ((':)
          *
          [Char]
          ((':)
             * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

Why is ghci doing the substitution for the type family, but not the type synonym? Is there a way to control when ghci will do the substitution?

The workaround that I know of is using :kind. For instance,

ghci> :kind (Container ‘[String,String,String,String,String])

Gives:

( Container ‘[String,String,String,String,String]) :: *

While

ghci> :kind! (Container ‘[String,String,String,String,String])

Will print something like this:
Container

((‘:)
```
  *
  [Char]
  ((':)
     * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))
```
Officially, of course, you’re asking ghci a different question with kind, but it works. Using undefined :: is sort of a workaround anyhow, so I thought this might suffice.

import GHC.TypeLits

data Container (xs::[*]) = Container

I load it up in ghci, then I type the following command:

:t undefined :: Container '[String,String,String,String,String]

Originally posted 2013-11-09 19:25:56.