(Originally reported [here](https://github.com/goldfirere/singletons/issues/405).) Here are two modules: ```hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeOperators #-} -- A stripped-down version of singletons module A where import Data.Kind (Type) import Data.Proxy (Proxy) data family Sing :: k -> Type class SingI a where sing :: Sing a class SingKind k where type Demote k = (r :: Type) | r -> k toSing :: Demote k -> Proxy k data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where type Demote (k1 ~> k2) = Demote k1 -> Demote k2 toSing = undefined withSing :: SingI a => (Sing a -> b) -> b withSing f = f sing ``` ```hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE AllowAmbiguousTypes #-} module LongTypeError where import A type family TypeFam f fun where TypeFam f (a -> b) = f a -> TypeFam f b lift :: (a -> b) -> TypeFam f (a -> b) lift f = \x -> _ (f <*> x) ``` If you try to run the following command using GHC 8.6.5, GHC 8.8.1, or HEAD: ``` $ /opt/ghc/8.6.5/bin/runghc LongTypeError.hs ``` You will be presented with one of the longest type errors in the history of type errors. The full thing is about 5,000 lines long, so here is an excerpt to give you a sense for how bad it is: ``` LongTypeError.hs:15:10: error: • Couldn't match type ‘f’ with ‘(->) a’ ‘f’ is a rigid type variable bound by the type signature for: lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b) at LongTypeError.hs:14:1-38 Expected type: TypeFam f (a -> b) Actual type: (a -> a) -> (a -> a) -> TypeFam ((->) a) ((a -> a) -> (a -> a -> a) -> (a -> a -> a -> a) -> Demote ((k1 ~> (k1 ~> (k1 ~> (k1 ~> k1)))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1)))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1))))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1)))))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1))))))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 ~> k1)))))))))) ~> ((k1 ~> (k1 ~> (k1 ~> (k1 ~> (k1 <elided> ~> k3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ~> k4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Actual type: a -> b • In the first argument of ‘(<*>)’, namely ‘f’ In the first argument of ‘_’, namely ‘(f <*> x)’ In the expression: _ (f <*> x) • Relevant bindings include x :: a -> a (bound at LongTypeError.hs:15:11) f :: a -> b (bound at LongTypeError.hs:15:6) lift :: (a -> b) -> TypeFam f (a -> b) (bound at LongTypeError.hs:15:1) | 15 | lift f = \x -> _ (f <*> x) | ^ ``` What is really curious about this example is that the `LongTypeError` module does not use anything from `A`. If you remove the `import A` line, you will instead get this much simpler error message: ``` LongTypeError.hs:15:10: error: • Couldn't match type ‘f’ with ‘(->) a’ ‘f’ is a rigid type variable bound by the type signature for: lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b) at LongTypeError.hs:14:1-38 Expected type: TypeFam f (a -> b) Actual type: (a -> a) -> (a -> a) -> TypeFam ((->) a) ((a -> a) -> (a -> a -> a) -> (a -> a -> a -> a) -> t0) • The lambda expression ‘\ x -> _ (f <*> x)’ has one argument, but its type ‘TypeFam f (a -> b)’ has none In the expression: \ x -> _ (f <*> x) In an equation for ‘lift’: lift f = \ x -> _ (f <*> x) • Relevant bindings include f :: a -> b (bound at LongTypeError.hs:15:6) lift :: (a -> b) -> TypeFam f (a -> b) (bound at LongTypeError.hs:15:1) | 15 | lift f = \x -> _ (f <*> x) | ^^^^^^^^^^^^^^^^^ LongTypeError.hs:15:16: error: • Found hole: _ :: (a -> b0) -> (a -> a) -> TypeFam ((->) a) b0 Where: ‘b0’ is an ambiguous type variable ‘a’ is a rigid type variable bound by the type signature for: lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b) at LongTypeError.hs:14:1-38 • In the expression: _ In the expression: _ (f <*> x) The lambda expression ‘\ x -> _ (f <*> x)’ has one argument, but its type ‘TypeFam f (a -> b)’ has none • Relevant bindings include x :: a -> a (bound at LongTypeError.hs:15:11) f :: a -> b (bound at LongTypeError.hs:15:6) lift :: (a -> b) -> TypeFam f (a -> b) (bound at LongTypeError.hs:15:1) | 15 | lift f = \x -> _ (f <*> x) | ^ LongTypeError.hs:15:19: error: • Couldn't match type ‘b’ with ‘a -> b0’ ‘b’ is a rigid type variable bound by the type signature for: lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b) at LongTypeError.hs:14:1-38 Expected type: a -> a -> (a -> a) -> (a -> a -> a) -> (a -> a -> a -> a) -> t0 Actual type: a -> b • In the first argument of ‘(<*>)’, namely ‘f’ In the first argument of ‘_’, namely ‘(f <*> x)’ In the expression: _ (f <*> x) • Relevant bindings include x :: a -> a (bound at LongTypeError.hs:15:11) f :: a -> b (bound at LongTypeError.hs:15:6) lift :: (a -> b) -> TypeFam f (a -> b) (bound at LongTypeError.hs:15:1) | 15 | lift f = \x -> _ (f <*> x) | ^ ```