Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,334
    • Issues 4,334
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 368
    • Merge Requests 368
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17139

Closed
Open
Opened Aug 30, 2019 by Ryan Scott@RyanGlScottMaintainer

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.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)
   |                   ^
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#17139