Opened 16 months ago

Closed 11 months ago

Last modified 6 months ago

#11339 closed bug (fixed)

Possible type-checker regression in GHC 8.0

Reported by: hvr Owned by: simonpj
Priority: highest Milestone: 8.0.2
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: Cc: simonpj, bgamari, Artyom.Kazak
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T11339, T11339b, T11339c, T11339d; partial-sigs/should_compile/T11339a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but not on GHC 8.0/8.1:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

module Failing where

import Control.Applicative ( Const(Const, getConst) )
import Data.Functor.Identity ( Identity(Identity) )

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
  [] -> right afb s
  _  -> t afb
  where
    -- t :: (a -> f b) -> f t

    -- TYPECHECKS with GHC 7.10, but not with GHC 8.x:
    Bazaar { getBazaar = t } = left sell s

    -- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:
    -- t = getBazaar (left sell s)

    sell :: a -> Bazaar a b b
    sell w   = Bazaar ($ w)

    pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]
    pins f   = getConst (f (\ra -> Const [Identity ra]))

newtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar $ \_ -> pure a
  Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb

The following error is emitted on GHC 8.0:

failing.hs:13:11: error:
    • Couldn't match type ‘f’ with ‘Const [Identity a]’
      ‘f’ is a rigid type variable bound by
        the type signature for:
          failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t
        at failing.hs:11:1
      Expected type: a -> Const [Identity a] b
        Actual type: a -> f b
    • In the first argument of ‘t’, namely ‘afb’
      In the expression: t afb
      In a case alternative: _ -> t afb
    • Relevant bindings include
        t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)
        sell :: a -> Bazaar a b b (bound at failing.hs:24:5)
        pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)
        afb :: a -> f b (bound at failing.hs:11:20)
        right :: Traversal s t a b (bound at failing.hs:11:14)
        left :: Traversal s t a b (bound at failing.hs:11:9)
        failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)

I don't understand why Bazaar t = ... vs t = getBazaar ... makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...

Change History (16)

comment:1 Changed 16 months ago by hvr

Owner: set to goldfire

Richard,

I threw git bisect at this issue, and the winner was 2db18b8135335da2da9918b722699df684097be9 (aka Visible Type Application)! :-)

Can you look at this and find out whether the type-checking failure is legitimate or not?

comment:2 Changed 16 months ago by goldfire

This is truly bizarre.

Here are a few things I've learned:

  1. The module compiles with -XNoMonomorphismRestriction. This is actually correct behavior. The issue is that the inferred type of t is quantified (by Applicative f). The monomorphism restriction forbids this. So the new behavior is correct, I think.
  1. Sadly, adding t :: Applicative f => (a -> f b) -> f t, by itself, doesn't fix the problem
  1. The line that you say doesn't compile does indeed compile if you add t :: Applicative f => (a -> f b) -> f t
  1. The line that you say doesn't compile does indeed compile if you add -XMonoLocalBinds.
  1. Saying t :: _ emits no warning. I have no idea why.

Here is some interpretation of the above:

  1. Fact (2) is a consequence of the fact that GHC considers itself to be inferring a type for all pattern bindings, even if there is a complete type signature. (See TcBinds.decideGeneralisationPlan) I don't know why this is the case; I did not change this behavior. Visible type application does a little extra jiggery pokery when inferring types. See Note [Instantiate when inferring a type] in TcBinds. This jiggery pokery is triggered because we're inferring the type of t, even when a type signature is given.
  1. Facts (3) and (4) (really the fact that the commented line doesn't compile in the first place) is because we're in the quite rare scenario where -XMonLocalBinds is a good idea, even absent type families / GADTs. This is not the first such example, but I don't have a link to a previous one. Perhaps RankNTypes should imply MonoLocalBinds.

Bottom line: The only real bug in here is (2). It really should compile with the type signature, regardless of the monomorphism restriction. But it doesn't. However, the example as submitted should be rejected, I believe.

comment:3 Changed 16 months ago by simonpj

Keywords: TypeInType added

comment:4 Changed 16 months ago by goldfire

Keywords: TypeInType removed

On further thought, (5) from comment:2 is a bug, too.

In any case, this one isn't my fault. I'm responsible for point (1) in comment:2, but that's an improvement (the file submitted ought not to be accepted, because it runs afoul of the monomorphism restriction).

On the other hand, points (2) and (5), the real bugs, are around in 7.10. With 7.10.2,

module Mono where

foo :: Show a => a -> String
(foo) = show

fails unless you enable -XNoMonomorphismRestriction. And

module Mono where

foo :: _
(foo) = id

succeeds, with no warnings.

I conjecture that both problems are related to the fact that decideGeneralisationPlan always infers for pattern bindings. But I haven't looked into it more than that.

comment:5 Changed 16 months ago by simonpj

Owner: changed from goldfire to simonpj

comment:6 Changed 15 months ago by bgamari

Version: 8.18.0.1-rc1

comment:7 Changed 13 months ago by simonpj

Interestingly, the code in the Description typechecks fine in HEAD.

comment:8 Changed 13 months ago by goldfire

So it does. How maddening. I don't know why. I stand by my analysis that the original program should be rejected according to the monomorphism restriction.

comment:9 Changed 13 months ago by Artyom.Kazak

Cc: Artyom.Kazak added

comment:10 Changed 13 months ago by simonpj

The stuff with partial type sigs (5) is related to #11670

comment:11 Changed 13 months ago by bgamari

Milestone: 8.0.18.0.2

This will not be addressed for 8.0.1. If you encounter this bug please add a type signature.

comment:12 Changed 13 months ago by RyanGlScott

This also affects machines. This is the code that is affected (simplified version reproduced below):

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- Simplified code from the machines package
module Data.Machine.Fanout where

class Semigroup a where
    (<>) :: a -> a -> a
    sconcat :: NonEmpty a -> a

data NonEmpty a = a :| [a]

-- | Witnessed type equality
data Is a b where
  Refl :: Is a a

-- | This is the base functor for a 'Machine' or 'MachineT'.
--
-- Note: A 'Machine' is usually constructed from 'Plan', so it does not need to be CPS'd.
data Step k o r
  = Stop
  | Yield o r
  | forall t. Await (t -> r) (k t) r

-- | A 'MachineT' reads from a number of inputs and may yield results before stopping
-- with monadic side-effects.
newtype MachineT m k o = MachineT { runMachineT :: m (Step k o (MachineT m k o)) }

-- | A @'ProcessT' m a b@ is a stream transducer that can consume values of type @a@
-- from its input, and produce values of type @b@ and has side-effects in the
-- 'Monad' @m@.
type ProcessT m a b = MachineT m (Is a) b

continue :: ([b] -> r) -> [(a -> b, b)] -> Step (Is a) o r
continue _ [] = Stop
continue f ws = Await (f . traverse fst ws) Refl (f $ map snd ws)

-- | Pack a 'Step' of a 'Machine' into a 'Machine'.
encased :: Monad m => Step k o (MachineT m k o) -> MachineT m k o
encased = MachineT . return

semigroupDlist :: Semigroup a => ([a] -> [a]) -> Maybe a
semigroupDlist f = case f [] of
  [] -> Nothing
  x:xs -> Just $ sconcat (x:|xs)

-- | Share inputs with each of a list of processes in lockstep. Any
-- values yielded by the processes are combined into a single yield
-- from the composite process.
fanout :: (Functor m, Monad m, Semigroup r)
       => [ProcessT m a r] -> ProcessT m a r
fanout = MachineT . go id id
  where
    go waiting acc [] = case waiting [] of
      ws -> return . maybe k (\x -> Yield x $ encased k) $ semigroupDlist acc
        where k = continue fanout ws
    go waiting acc (m:ms) = runMachineT m >>= \v -> case v of
      Stop           -> go waiting acc ms
      Yield x k      -> go waiting (acc . (x:)) (k:ms)
      Await f Refl k -> go (waiting . ((f, k):)) acc ms

-- | Share inputs with each of a list of processes in lockstep. If
-- none of the processes yields a value, the composite process will
-- itself yield 'mempty'. The idea is to provide a handle on steps
-- only executed for their side effects. For instance, if you want to
-- run a collection of 'ProcessT's that await but don't yield some
-- number of times, you can use 'fanOutSteps . map (fmap (const ()))'
-- followed by a 'taking' process.
fanoutSteps :: (Functor m, Monad m, Monoid r)
            => [ProcessT m a r] -> ProcessT m a r
fanoutSteps = MachineT . go id id
  where
    go waiting acc [] = case (waiting [], mconcat (acc [])) of
      (ws, xs) -> return . Yield xs $ encased (continue fanoutSteps ws)
    go waiting acc (m:ms) = runMachineT m >>= \v -> case v of
      Stop           -> go waiting acc ms
      Yield x k      -> go waiting (acc . (x:)) (k:ms)
      Await f Refl k -> go (waiting . ((f, k):)) acc ms

The workaround is to change the definitions of fanout and fanoutSteps to the following:

-- | Share inputs with each of a list of processes in lockstep. Any
-- values yielded by the processes are combined into a single yield
-- from the composite process.
fanout :: forall m a r. (Functor m, Monad m, Semigroup r)
       => [ProcessT m a r] -> ProcessT m a r
fanout = MachineT . go id id
  where
    go :: ([(a -> ProcessT m a r, ProcessT m a r)]
       -> [(a -> ProcessT m a r, ProcessT m a r)])
       -> ([r] -> [r])
       -> [ProcessT m a r]
       -> m (Step (Is a) r (ProcessT m a r))
    go waiting acc [] = case waiting [] of
      ws -> return . maybe k (\x -> Yield x $ encased k) $ semigroupDlist acc
        where k = continue fanout ws
    go waiting acc (m:ms) = runMachineT m >>= \v -> case v of
      Stop           -> go waiting acc ms
      Yield x k      -> go waiting (acc . (x:)) (k:ms)
      Await f Refl k -> go (waiting . ((f, k):)) acc ms

-- | Share inputs with each of a list of processes in lockstep. If
-- none of the processes yields a value, the composite process will
-- itself yield 'mempty'. The idea is to provide a handle on steps
-- only executed for their side effects. For instance, if you want to
-- run a collection of 'ProcessT's that await but don't yield some
-- number of times, you can use 'fanOutSteps . map (fmap (const ()))'
-- followed by a 'taking' process.
fanoutSteps :: forall m a r. (Functor m, Monad m, Monoid r)
            => [ProcessT m a r] -> ProcessT m a r
fanoutSteps = MachineT . go id id
  where
    go :: ([(a -> ProcessT m a r, ProcessT m a r)]
       -> [(a -> ProcessT m a r, ProcessT m a r)])
       -> ([r] -> [r])
       -> [ProcessT m a r]
       -> m (Step (Is a) r (ProcessT m a r))
    go waiting acc [] = case (waiting [], mconcat (acc [])) of
      (ws, xs) -> return . Yield xs $ encased (continue fanoutSteps ws)
    go waiting acc (m:ms) = runMachineT m >>= \v -> case v of
      Stop           -> go waiting acc ms
      Yield x k      -> go waiting (acc . (x:)) (k:ms)
      Await f Refl k -> go (waiting . ((f, k):)) acc ms

comment:13 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In 15b9bf4b/ghc:

Improve typechecking of let-bindings

This major commit was initially triggered by #11339, but it spiraled
into a major review of the way in which type signatures for bindings
are handled, especially partial type signatures.  On the way I fixed a
number of other bugs, namely
   #12069
   #12033
   #11700
   #11339
   #11670

The main change is that I completely reorganised the way in which type
signatures in bindings are handled. The new story is in TcSigs
Note [Overview of type signatures].  Some specific:

* Changes in the data types for signatures in TcRnTypes:
  TcIdSigInfo and new TcIdSigInst

* New module TcSigs deals with typechecking type signatures
  and pragmas. It contains code mostly moved from TcBinds,
  which is already too big

* HsTypes: I swapped the nesting of HsWildCardBndrs
  and HsImplicitBndsrs, so that the wildcards are on the
  oustide not the insidde in a LHsSigWcType.  This is just
  a matter of convenient, nothing deep.

There are a host of other changes as knock-on effects, and
it all took FAR longer than I anticipated :-).  But it is
a significant improvement, I think.

Lots of error messages changed slightly, some just variants but
some modest improvements.

New tests

* typecheck/should_compile
    * SigTyVars: a scoped-tyvar test
    * ExPat, ExPatFail: existential pattern bindings
    * T12069
    * T11700
    * T11339

* partial-sigs/should_compile
    * T12033
    * T11339a
    * T11670

One thing to check:

* Small change to output from ghc-api/landmines.
  Need to check with Alan Zimmerman

comment:14 Changed 11 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T11339, T11339b, T11339c, T11339d; partial-sigs/should_compile/T11339a

This is a complicated ticket, and I've spent an unreasonably long time on the patch. But I'm very happy with the result.

There are a number of separate strands

  • comment:12, I think fanout definitely needs a type signature for go. Look at the GADT pattern match on Refl in the Await branch... GADTs always need a type signature! I have no idea how 7.10 compiled this program; maybe a bug!
  • Difference between these two bindings:
        Bazaar { getBazaar = t } = left sell s
    
        t = getBazaar (left sell s)
    
    Well, the first falls under the Monomorphism Restriction, while the second does not. Simple as that.
  • comment:4, item (2). I disagree:
    foo :: Show a => a -> String
    (foo) = show
    
    Here the binding falls under the monomorphism restriction, and cannot be rescued by a type signature. Test: typecheck/should_compile/T11339
        • Overloaded signature conflicts with monomorphism restriction
            t :: forall (f :: * -> *). Applicative f => (a -> f b) -> f t
    
    Adding -XNoMonomorhismRestriction makes it fine. Test: typecheck/should_compile/T11339b
  • comment:4, item (5), yes this was a bad bug
    foo :: _
    (foo) = id
    
    Fixed: test is partial-sigs/should_compile/T11339a

Tricky stuff.

comment:15 Changed 11 months ago by goldfire

Agreed about comment:4 item (2): it does hit the MR, when reading the Report closely. I hadn't known that the MR struck annotated variables if they are bound in a pattern binding.

Otherwise, hooray! This does seem all fixed now -- including rejecting (once again) the original program in the description. (That should be rejected as it correctly runs afoul of the MR.)

Thanks! :)

comment:16 Changed 6 months ago by Simon Peyton Jones <simonpj@…>

In 45bfd1a/ghc:

Refactor typechecking of pattern bindings

This patch fixes a regression introduced, post 8.0.1, by
this major commit:

     commit 15b9bf4ba4ab47e6809bf2b3b36ec16e502aea72
     Author: Simon Peyton Jones <simonpj@microsoft.com>
     Date:   Sat Jun 11 23:49:27 2016 +0100

         Improve typechecking of let-bindings

         This major commit was initially triggered by #11339, but it
         spiraled into a major review of the way in which type
         signatures for bindings are handled, especially partial type
         signatures.

I didn't get the typechecking of pattern bindings right, leading
to Trac #12427.

In fixing this I found that this program doesn't work:

  data T where
    T :: a -> ((forall b. [b]->[b]) -> Int) -> T

  h1 y = case y of T _ v -> v

Works in 7.10, but not in 8.0.1.

There's a happy ending. I found a way to fix this, and improve
pattern bindings too.  Not only does this fix #12427, but it also
allows

In particular,we now can accept

  data T where MkT :: a -> Int -> T

  ... let { MkT _ q = t } in ...

Previously this elicited "my head exploded" but it's really
fine since q::Int.

The approach is described in detail in TcBinds
   Note [Typechecking pattern bindings]
Super cool.  And not even a big patch!
Note: See TracTickets for help on using tickets.