Enormous error message when importing seemingly unused module
(Originally reported here.)
Here are two modules:
{-# 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{-# 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.hsYou 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)
| ^