A GHCi command to normalize TyCon declarations at user given types and print them

Disclaimer

The following design is an early draft for an idea regarding a new GHCi command called normalise. Everything down to the command name is susceptible to change.

For lack of a better word, throughout the text, I'll refer to the process of expanding type synonyms and applying type-family reductions as normalisation.

Quick Summary

Assume you've loaded the following declarations in GHCi.

data D1 f a b
  = MkD11 (f a b)
  | MkD12 (f b a)
  | MkD13 (Either a (MaybeT (f String) b))

type family T1 a where
  T1 Int = String
  T1 Bool = Char
  T1 Double = Integer
  T1 Integer = Bool
  T1 Char = Double
  T1 String = Int
  T1 a = Maybe a

data D2 a b c = MkD2 (T1 a) (T1 b) (T1 c) a b c

data D3 a b where
  MkD31 :: forall x y. (x ~ String, x ~ y) => x -> y -> D3 x x

Now you can ask for the exact shape of these declarations at different instantiations.

-- :normalise (D2 Int b c) or :normalise (D2 Int)
type role D2 nominal nominal
type D2 :: * -> * -> *
data D2 b c = MkD2 String (T1 b) (T1 c) Int b c

-- The variant with exclamation mark removes constraints that have all their free variables instantiated.
-- :normalise! (D3 String String)
type D3 :: *
data D3 where
  MKG31 :: forall y. String ~ y => String -> y -> D3

-- :normalise (D1 Either a Bool)
data D1 a
  = MkD11 (Either a Bool)
  | MkD12 (Either Bool a)
  | MkD13 (Either a (MaybeT (Either String) Bool))

Motivation

Seeing the exact shape of declarations in different stages of the program. This comes very handy when the declarations are TTG datatypes.

Usage guide

There are two variations of the normalise command.

• normalise: After normalizing the input itself, instantiates the universals of the resulting application at the types given by the user. And normalises the results when possible.
• normalise!: Ditto, except it also removes fully instantiated constraints.

The arguments of the normalise command should always appear inside parenthesis. Otherwise given the input Either Bool Int, normalise wouldn't be able to know if you are looking for the normalised version of "Either, Bool, and Int", "Either Bool, and Int", or "Either Bool Int".

Spec

Given the input (h args), where args could be empty:

1. Fully normalize the application to get h' ty_1 ... ty_n
2. Assuming TyCon h' has binders (b_1 ... b_n), create a substitution omega = [b_i := ty_i] where 1 <= i <= n.
3. Apply omega to the data constructors of h', and then expand all the type synonyms, and do all the possible type family reductions.
4. Get rid of the data constructors that don't have the return type h' ty_1 ... ty_n; which is quite common in the case of GADT declarations.
5. Print the resulting kind, and the resulting declaration of the type constructor.