#15928: Reduction stack overflow when using "coerce" -------------------------------------+------------------------------------- Reporter: harendra | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by harendra): I think GHC needs to move on from "by GHC developers for GHC developers" to "by GHC developers for mortal Haskell programmers". You have a lot more context here than a Haskell programmer at large would have. The error needs to be resolved quickly, in a few seconds or perhaps minutes would be fine too. The error message and the documentation does not serve that purpose, it (Data.Coerce) refers to the paper and the roles wiki page (referring to papers is common theme for GHC and Haskell libraries), the paper is accessible to only a very small population, and we should not expect a large population of programmers to go read the paper and spend hours or even days or weeks trying to understand it and having to learning a lot of other things in the process. For that one error message, which can be explained better in just a few more words, it becomes a big digression. I am sorry about that rant, GHC devs are doing a terrific job, it is a wonderful technology but it has a potential to become much more usable by a lot more ordinary programmers like me if the error messages and the documentation become a little better. Keeping that aside, I still have a few questions about the issue at hand, I suspect there is a bug here: 1) Why a and a0 are treated as different types in the first version of the code? If a ~ a0 then there won't be a loop. In fact, this code is coercing a type into itself, which should be trivial. In the second version of the code where it works, the two types have been explicitly forced to be the same via a type signature. 2) This code works fine if the "Stream" type is defined using "data" instead of a "newtype". It puzzles me, why in that case we are not going into a loop? Why in that case the types a and a0 are the same? About the error message, I think it can be improved. First of all, a regular programmer won't have any idea what a "reduction stack" is, they can just guess, it is possibly a GHC internal thing. The error message is for GHC developers, not for users. The flag "-freduction-depth" is only mentioned in "Undecidable Instances section" of the guide, nowhere else. If the programmer is supposed to know about the reduction stack then it should be documented and the concept should be explained. But I guess we can do better even without doing that. The error message can perhaps be phrased something like this, it might be inaccurate, but just to give an idea: {{{ When trying to determine that the representation of type x is the same as that of type y, we expanded the types n times but still could not determine that they are equal, we can go on but we are limited by the reduction stack size which can be changed by using the -freduction-depth option. In some cases where the types are recursively defined, it is possible that the expansion forms an infinite loop that never terminates. For more details and examples see this manual page. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15928#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Would you (for any value of "you") care to write some? Considering the case "you" == "me", in fact my (tiny) personal contribution to GHC started with documentation. Though I would love to do

#15928: Reduction stack overflow when using "coerce" -------------------------------------+------------------------------------- Reporter: harendra | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by harendra): that more unfortunately due to lack of funding I cannot devote time on this.

There's no reason for GHC to assume that a and a0 should be the same, so it doesn't

I am a bit puzzled, initially I thought the same, but then I wondered why GHC treats them the same in the case when `Stream` is not a newtype. So there seems to be a contradiction here, and that is the origin of this issue, because it was working in one case but not in the other, and it was working with explicit type annotation. Let's start with the types `SerialT Identity a` and `SerialT Identity a0`. In the "data Stream" case it would get expanded to: {{{ Stream Identity a Stream Identity a0 }}} Now why does GHC think that these two types are equal if it thinks `a` is not the same as `a0`. I am sure I am missing something, so please help me understand. Maybe after the representations have been simplified GHC is able to unify a with a0. In the problematic case it is never able to simplify them in the first place so the question of unifying never comes. If ultimately `a` can anyway be unified with `a0` then can it unify them before simplifying? In the explicit annotation case perhaps that is what is happening, the programmer has already told GHC that `a` and `a0` are the same, so the simplification starts with that assumption. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15928#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15928: Reduction stack overflow when using "coerce" -------------------------------------+------------------------------------- Reporter: harendra | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): If we ask GHC for the role signature on `Stream` (as you can with `:info` in GHCi), we learn that the `a` parameter has a phantom role. This means that `Stream Identity a` shares a representation with `Stream Identity a0` no matter what `a` and `a0` are. So GHC does not unify them. Instead, it simply doesn't care what `a0` is. It chooses `Any`. (We can see this with `-ddump-tc -fprint-typechecker-elaboration`). When you change the definition for `Stream`, `a` then gets a representational role, and so GHC is stuck trying to figure out what `a0` is, giving you the error you observe. If you say `type role Stream representational nominal`, then the program is accepted, because now GHC observes that `a0` must certainly be `a`. It does the unification and then succeeds.

If there is no bug then this needs to be explained in some simple way.

I respectfully disagree with this statement. Though simplicity is always a goal, it cannot be achieved in all cases. In the end, the `coerce` feature was added to provide a performance boost when GHC can know that runtime representations of two types are the same. That knowledge -- i.e., knowing when two types are `Coercible` -- is subtle, which is why it took the research community three papers to figure it out. Even now, as you have observed, we have room to improve. (That is, the choice between `data` and `newtype` shouldn't matter here... but it does, because we don't know an algorithm that can work reliably with recursive newtypes.) One might argue that we should have never introduced `coerce` because the theory behind it is too complicated. For better or worse, the Haskell community tends to prefer complicated, powerful solutions over simple, less expressive ones. (Of course, we love simple, powerful ones!) And so we end up where we are today. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15928#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15928: Improve error message: Reduction stack overflow when using "coerce" -------------------------------------+------------------------------------- Reporter: harendra | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:

Compiling the following snippet results in a "Reduction stack overflow" error message:

{{{#!hs {-# Language ScopedTypeVariables #-} {-# Language RankNTypes #-}

import Data.Functor.Identity import Data.Coerce

newtype Stream m a = Stream { unStream :: forall r. (Stream m a -> m r) -> m r }

newtype SerialT m a = SerialT (Stream m a)

g :: SerialT Identity a -> Identity Bool g m = undefined

idSerial :: SerialT Identity a -> SerialT Identity a idSerial = id

f :: SerialT Identity a -> Identity Bool f = g . idSerial . coerce

main = undefined }}}

The following error message is produced on compiling this with ghc-8.6.2:

{{{ xy.hs:26:20: error: • Reduction stack overflow; size = 201 When simplifying the following type: Coercible ((Stream Identity a -> Identity r) -> Identity r) ((Stream Identity a0 -> Identity r) -> Identity r) 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 second argument of ‘(.)’, namely ‘coerce’ In the second argument of ‘(.)’, namely ‘idSerial . coerce’ In the expression: g . idSerial . coerce | 26 | f = g . idSerial . coerce | ^^^^^^ }}}

When I use an inline signature like this:

{{{#!hs f :: SerialT Identity a -> Identity Bool f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce

main = undefined }}}

It again results in the same error:

{{{ xy.hs:18:60: error: • Reduction stack overflow; size = 201 When simplifying the following type: Coercible ((Stream Identity a -> Identity r) -> Identity r) ((Stream Identity a0 -> Identity r) -> Identity r) 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 second argument of ‘(.)’, namely ‘coerce’ In the second argument of ‘(.)’, namely ‘(id :: SerialT Identity a -> SerialT Identity a) . coerce’ In the expression: g . (id :: SerialT Identity a -> SerialT Identity a) . coerce | 18 | f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce | ^^^^^^ }}}

Everything works fine is I use an inline signature with a `forall` keyword like this:

{{{#!hs f :: forall a. SerialT Identity a -> Identity Bool f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce }}}

I have following questions:

1) Why the first version results in a panic? Is that a bug? 2) The second version might possibly be incorrect code because the types do not unify, but still it should not result in a panic, because of the panic I could not figure out what the problem is. It took a long time to isolate the code and then do some trial and error on it.

New description: EDIT: Executive summary: The error messages below are confusing and not perspicuous to users. We should fix. comment:2 has a concrete suggestion to use as a starting point, and comment:7 suggests we print out the role signature of any tycons involved. Compiling the following snippet results in a "Reduction stack overflow" error message: {{{#!hs {-# Language ScopedTypeVariables #-} {-# Language RankNTypes #-} import Data.Functor.Identity import Data.Coerce newtype Stream m a = Stream { unStream :: forall r. (Stream m a -> m r) -> m r } newtype SerialT m a = SerialT (Stream m a) g :: SerialT Identity a -> Identity Bool g m = undefined idSerial :: SerialT Identity a -> SerialT Identity a idSerial = id f :: SerialT Identity a -> Identity Bool f = g . idSerial . coerce main = undefined }}} The following error message is produced on compiling this with ghc-8.6.2: {{{ xy.hs:26:20: error: • Reduction stack overflow; size = 201 When simplifying the following type: Coercible ((Stream Identity a -> Identity r) -> Identity r) ((Stream Identity a0 -> Identity r) -> Identity r) 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 second argument of ‘(.)’, namely ‘coerce’ In the second argument of ‘(.)’, namely ‘idSerial . coerce’ In the expression: g . idSerial . coerce | 26 | f = g . idSerial . coerce | ^^^^^^ }}} When I use an inline signature like this: {{{#!hs f :: SerialT Identity a -> Identity Bool f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce main = undefined }}} It again results in the same error: {{{ xy.hs:18:60: error: • Reduction stack overflow; size = 201 When simplifying the following type: Coercible ((Stream Identity a -> Identity r) -> Identity r) ((Stream Identity a0 -> Identity r) -> Identity r) 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 second argument of ‘(.)’, namely ‘coerce’ In the second argument of ‘(.)’, namely ‘(id :: SerialT Identity a -> SerialT Identity a) . coerce’ In the expression: g . (id :: SerialT Identity a -> SerialT Identity a) . coerce | 18 | f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce | ^^^^^^ }}} Everything works fine is I use an inline signature with a `forall` keyword like this: {{{#!hs f :: forall a. SerialT Identity a -> Identity Bool f = g . (id :: SerialT Identity a -> SerialT Identity a) . coerce }}} I have following questions: 1) Why the first version results in a panic? Is that a bug? 2) The second version might possibly be incorrect code because the types do not unify, but still it should not result in a panic, because of the panic I could not figure out what the problem is. It took a long time to isolate the code and then do some trial and error on it. -- Comment (by goldfire): Yes, by all means we can improve that error message, and we should leave this ticket open as an opportunity to do so. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15928#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler