Regression: HEAD incurs a reduction stack overflow on program involving type equality
Originally observed in a head.hackage
build here.
The following code, minimized from the plots-0.1.1.2
library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957) but does typecheck with GHC 8.10.2 and 9.0.1-alpha1:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Plots.Types where
import Data.Functor
import Data.Typeable
type family N a
data StyledPlot n where
StyledPlot :: Typeable p => p -> StyledPlot (N p)
styledPlot :: forall p f.
(Typeable p, Applicative f)
=> (p -> f p)
-> StyledPlot (N p) -> f (StyledPlot (N p))
styledPlot f s@(StyledPlot p) =
case eq p of
Just Refl -> f p <&> \p' -> StyledPlot p'
Nothing -> pure s
where eq :: Typeable a => a -> Maybe (a :~: p)
eq _ = eqT
On HEAD, this produces the following error:
$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Plots.Types ( Bug.hs, Bug.o )
Bug.hs:21:33: error:
• Reduction stack overflow; size = 201
When simplifying the following type: N p1
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: StyledPlot p'
In the second argument of ‘(<&>)’, namely ‘\ p' -> StyledPlot p'’
In the expression: f p <&> \ p' -> StyledPlot p'
|
21 | Just Refl -> f p <&> \p' -> StyledPlot p'
| ^^^^^^^^^^^^^