Skip to content
Snippets Groups Projects

GHC hangs during type-checking

    • Closed Issue created by Isaac Elliott @LightAndLight

    GHC 8.0.2 doesn't terminate when type checking this file:

    import           Control.Lens
import           Data.Functor.Compose

traverseCompose :: (a -> f b) -> g a -> f (h _)
traverseCompose = _Wrapping Compose . traverse

    This is the smallest type signature I could find that still causes the problem. GHCi infers the type without issue, and when I annotate it with the correct type signature, the file is successfully compiled.

    Using base-4.9.1.0, lens-4.14.1, and transformers-0.5.2.0

    Trac metadata
    Trac field Value
    Version 8.0.2
    Type Bug
    TypeOfFailure OtherFailure
    Priority normal
    Resolution Unresolved
    Component Compiler
    Test case
    Differential revisions
    BlockedBy
    Related
    Blocking
    CC
    Operating system
    Architecture
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items 0

    • No child items are currently assigned. Use child items to break down this issue into smaller parts.

    Activity

    • Isaac Elliott changed weight to 5

      changed weight to 5

    • Isaac Elliott added Tbug Trac import labels

      added Tbug Trac import labels

    • Ryan Scott mentioned in issue #14173 (closed)

      mentioned in issue #14173 (closed)

    • Simon Peyton Jones
      Simon Peyton Jones @simonpj ·
      Developer

      Seems to work OK with HEAD.

      What about with 8.2?

      With HEAD I get

      T14172.hs:7:19: error:
    • Occurs check: cannot construct the infinite type: a ~ g'1 a
      Expected type: (f'0 a -> f (f'0 b))
                     -> Compose f'0 g'1 a -> f (h a')
        Actual type: (Unwrapped (Compose f'0 g'1 a)
                      -> f (Unwrapped (h a')))
                     -> Compose f'0 g'1 a -> f (h a')
    • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
      In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
    • Relevant bindings include
        traverseCompose :: (a -> f b) -> g a -> f (h a')
          (bound at T14172.hs:7:1)
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^

T14172.hs:7:19: error:
    • Couldn't match type ‘g’ with ‘Compose f'0 g'1’
      ‘g’ is a rigid type variable bound by
        the inferred type of
        traverseCompose :: (a -> f b) -> g a -> f (h a')
        at T14172.hs:7:1-46
      Expected type: (a -> f b) -> g a -> f (h a')
        Actual type: (a -> f b) -> Compose f'0 g'1 a -> f (h a')
    • In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
    • Relevant bindings include
        traverseCompose :: (a -> f b) -> g a -> f (h a')
          (bound at T14172.hs:7:1)
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    • Ryan Scott
      Ryan Scott @RyanGlScott ·
      Maintainer

      So this is odd. I tried running the example file (after installing the lens package) on GHC 8.2.1, and while it didn't loop forever, it //did// stack overflow:

      $ /opt/ghc/8.2.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

Foo.hs:7:19: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: g ~ Compose f'0 g'0
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

      Which certainly isn't good. I then tried to remove external dependencies:

      {-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Lens where

import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
  (#.) :: Coercible c b => (b -> c) -> p a b -> p a c

instance Profunctor (->) where
  dimap ab cd bc = cd . bc . ab
  {-# INLINE dimap #-}
  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
  {-# INLINE (#.) #-}

type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
type Iso' s a = Iso s s a a

iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso sa bt = dimap sa (fmap bt)
{-# INLINE iso #-}

type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)

data Exchange a b s t = Exchange (s -> a) (b -> t)

instance Profunctor (Exchange a b) where
  dimap f g (Exchange sa bt) = Exchange (sa . f) (g . bt)
  {-# INLINE dimap #-}
  (#.) _ = coerce
  {-# INLINE ( #. ) #-}

withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso ai k = case ai (Exchange id Identity) of
  Exchange sa bt -> k sa (runIdentity #. bt)
{-# INLINE withIso #-}

class Wrapped s where
  type Unwrapped s :: *
  _Wrapped' :: Iso' s (Unwrapped s)

class Wrapped s => Rewrapped (s :: *) (t :: *)

class    (Rewrapped s t, Rewrapped t s) => Rewrapping s t
instance (Rewrapped s t, Rewrapped t s) => Rewrapping s t

instance (t ~ Compose f' g' a') => Rewrapped (Compose f g a) t
instance Wrapped (Compose f g a) where
  type Unwrapped (Compose f g a) = f (g a)
  _Wrapped' = iso getCompose Compose

_Wrapping :: Rewrapping s t => (Unwrapped s -> s) -> Iso s t (Unwrapped s) (Unwrapped t)
_Wrapping _ = _Wrapped
{-# INLINE _Wrapping #-}

_Wrapped :: Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped = withIso _Wrapped' $ \ sa _ -> withIso _Wrapped' $ \ _ bt -> iso sa bt
{-# INLINE _Wrapped #-}
      module Bug where

import Data.Functor.Compose
import Lens

traverseCompose :: (a -> f b) -> g a -> f (h _)
traverseCompose = _Wrapping Compose . traverse

      However, once I do that, compiling with GHC 8.2.1 no longer stack overflows!

      $ /opt/ghc/8.2.1/bin/ghc -c -O Lens.hs
$ /opt/ghc/8.2.1/bin/ghc -c -O Bug.hs

Bug.hs:6:46: error:
    • Found type wildcard ‘_’ standing for ‘a'’
      Where: ‘a'’ is a rigid type variable bound by
               the inferred type of
               traverseCompose :: (a -> f b) -> g a -> f (h a')
               at Bug.hs:7:1-46
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature:
        traverseCompose :: (a -> f b) -> g a -> f (h _)
  |
6 | traverseCompose :: (a -> f b) -> g a -> f (h _)
  |                                              ^

Bug.hs:7:19: error:
    • Occurs check: cannot construct the infinite type: a ~ g'1 a
      Expected type: (f'0 a -> f (f'0 b))
                     -> Compose f'0 g'1 a -> f (h a')
        Actual type: (Unwrapped (Compose f'0 g'1 a)
                      -> f (Unwrapped (h a')))
                     -> Compose f'0 g'1 a -> f (h a')
    • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
      In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
    • Relevant bindings include
        traverseCompose :: (a -> f b) -> g a -> f (h a')
          (bound at Bug.hs:7:1)
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^

Bug.hs:7:19: error:
    • Couldn't match type ‘g’ with ‘Compose f'0 g'1’
      ‘g’ is a rigid type variable bound by
        the inferred type of
        traverseCompose :: (a -> f b) -> g a -> f (h a')
        at Bug.hs:7:1-46
      Expected type: (a -> f b) -> g a -> f (h a')
        Actual type: (a -> f b) -> Compose f'0 g'1 a -> f (h a')
    • In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
    • Relevant bindings include
        traverseCompose :: (a -> f b) -> g a -> f (h a')
          (bound at Bug.hs:7:1)
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

      So for some reason, this bug only seems to pop up when lens is installed as a library. I'm stumped.

    • Ryan Scott
      Ryan Scott @RyanGlScott ·
      Maintainer

      Aha! The fault was on my end, as I forgot to put PolyKinds into Lens.hs. After doing that, I can reproduce the stack overflow with these two files:

      {-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Lens where

import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
  (#.) :: Coercible c b => (b -> c) -> p a b -> p a c

instance Profunctor (->) where
  dimap ab cd bc = cd . bc . ab
  {-# INLINE dimap #-}
  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
  {-# INLINE (#.) #-}

type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
type Iso' s a = Iso s s a a

iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso sa bt = dimap sa (fmap bt)
{-# INLINE iso #-}

type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)

data Exchange a b s t = Exchange (s -> a) (b -> t)

instance Profunctor (Exchange a b) where
  dimap f g (Exchange sa bt) = Exchange (sa . f) (g . bt)
  {-# INLINE dimap #-}
  (#.) _ = coerce
  {-# INLINE ( #. ) #-}

withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso ai k = case ai (Exchange id Identity) of
  Exchange sa bt -> k sa (runIdentity #. bt)
{-# INLINE withIso #-}

class Wrapped s where
  type Unwrapped s :: *
  _Wrapped' :: Iso' s (Unwrapped s)

class Wrapped s => Rewrapped (s :: *) (t :: *)

class    (Rewrapped s t, Rewrapped t s) => Rewrapping s t
instance (Rewrapped s t, Rewrapped t s) => Rewrapping s t

instance (t ~ Compose f' g' a') => Rewrapped (Compose f g a) t
instance Wrapped (Compose f g a) where
  type Unwrapped (Compose f g a) = f (g a)
  _Wrapped' = iso getCompose Compose

_Wrapping :: Rewrapping s t => (Unwrapped s -> s) -> Iso s t (Unwrapped s) (Unwrapped t)
_Wrapping _ = _Wrapped
{-# INLINE _Wrapping #-}

_Wrapped :: Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped = withIso _Wrapped' $ \ sa _ -> withIso _Wrapped' $ \ _ bt -> iso sa bt
{-# INLINE _Wrapped #-}
      module Bug where

import Data.Functor.Compose
import Lens

traverseCompose :: (a -> f b) -> g a -> f (h _)
traverseCompose = _Wrapping Compose . traverse
      $ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Lens             ( Lens.hs, interpreted )
[2 of 2] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:7:19: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type: g ~ Compose f'0 g'0
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: _Wrapping Compose . traverse
      In an equation for ‘traverseCompose’:
          traverseCompose = _Wrapping Compose . traverse
  |
7 | traverseCompose = _Wrapping Compose . traverse
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

      So now for the magic question: what fixed this in HEAD?

    • Simon Peyton Jones
      Simon Peyton Jones @simonpj ·
      Developer

      So now for the magic question: what fixed this in HEAD?

      You are busy bisecting?

    • Ryan Scott
      Ryan Scott @RyanGlScott ·
      Maintainer

      Indeed. My hunch is one of Richard's recent commits... I'll report back when I've confirmed it.

    • Ryan Scott
      Ryan Scott @RyanGlScott ·
      Maintainer

      Well I'll be... the commit that fixed it was not what I was expecting: 433b80de (Ensure that insolubles are fully rewritten).

    • Ryan Scott mentioned in commit 00f7e285

      mentioned in commit 00f7e285

    • Ryan Scott closed

      closed

    • Ryan Scott
      Ryan Scott @RyanGlScott ·
      Maintainer

      Oops, I forgot about this! I just committed a regression test, so this can be closed.

      Trac metadata
      Trac field Value
      Resolution Unresolved → ResolvedFixed
      Test case - → polykinds/T14172
    • trac-import added compiler crash label

      added compiler crash label

    • Ben Gamari added Pnormal label

      added Pnormal label

    Please register or sign in to reply