Is it possible to normalize a type that contains free type variables in Haskell?

user_12391863 0
Viewed 96

My goal is similar to this question: I would like to normalize a type in GHCi. But the type contains free type variables. For example, the type

StM (ExceptT e m) a

should normalize to

StM m (Either e a)

But when I typed !k StM (ExceptT e m) a into GHCi, it complained about those free type variables. Are there any other ways of doing so in Haskell?

type-families type-level-computation haskell
1 Answers
> import Control.Monad.Except
> :set -XTypeFamilies -XUndecidableInstances
> type family StM f a where StM (ExceptT e m) a = StM m (Either e a)

You can use partial types _, it's unfortunate it gets printed as GHC.Types.Any:

> :set -XPartialTypeSignatures -Wno-partial-type-signatures
> :kind! StM (ExceptT _ _) _
StM (ExceptT _ _) _ :: *
= StM Any (Either Any Any)

but it also works if you find concrete types

> :kind! StM (ExceptT String []) Int
StM (ExceptT String []) Int :: *
= StM [] (Either [Char] Int)

or you can quantify explicitly

> :set -XRankNTypes
> :kind! forall m e a. StM (ExceptT e m) a
forall m e a. StM (ExceptT e m) a :: *
= StM m (Either e a)

I think it would be a good feature to implicitly quantify for :kind so you can write :kind StM (ExceptT e m) a and it inserts the foralls for you.

user_1658060
Related