Opened 2 years ago

Closed 2 years ago

#14327 closed bug (duplicate)

Type error in program caused by unrelated definition

Reported by: lexi.lambda Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: FunDeps Cc: dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #13506 Differential Rev(s):
Wiki Page:

Description

Adapted from this Stack Overflow question.

The following program raises two type errors:

import Prelude hiding (readFile, writeFile)
import Control.Monad.Free
import Data.Functor.Sum

data FileSystemF a
  = ReadFile FilePath (String -> a)
  | WriteFile FilePath String a
  deriving (Functor)

data ConsoleF a
  = WriteLine String a
  deriving (Functor)

data CloudF a
  = GetStackInfo String (String -> a)
  deriving (Functor)

type App = Free (Sum FileSystemF (Sum ConsoleF CloudF))

readFile :: FilePath -> App String
readFile path = liftF (InL (ReadFile path id))

writeFile :: FilePath -> String -> App ()
writeFile path contents = liftF (InL (WriteFile path contents ()))

writeLine :: String -> App ()
writeLine line = liftF (InR (WriteLine line ()))
/private/tmp/free-sandbox/src/FreeSandbox.hs:26:27: error:
    • Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’
        arising from a functional dependency between constraints:
          ‘MonadFree
             (Sum FileSystemF (Sum ConsoleF CloudF))
             (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’ at src/FreeSandbox.hs:26:27-66
          ‘MonadFree
             (Sum FileSystemF ConsoleF)
             (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’ at src/FreeSandbox.hs:29:18-48
    • In the expression: liftF (InL (WriteFile path contents ()))
      In an equation for ‘writeFile’:
          writeFile path contents = liftF (InL (WriteFile path contents ()))
   |
26 | writeFile path contents = liftF (InL (WriteFile path contents ()))
   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

/private/tmp/free-sandbox/src/FreeSandbox.hs:29:18: error:
    • Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’
        arising from a functional dependency between:
          constraint ‘MonadFree
                        (Sum FileSystemF ConsoleF)
                        (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’
          instance ‘MonadFree f (Free f)’ at <no location info>
    • In the expression: liftF (InR (WriteLine line ()))
      In an equation for ‘writeLine’:
          writeLine line = liftF (InR (WriteLine line ()))
   |
29 | writeLine line = liftF (InR (WriteLine line ()))
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The second of the two errors (the one on line 29) makes sense—it’s an error I would expect (there is a missing use of InL). However, the first error seems incorrect, as the definition of writeFile is, in fact, well-typed. In fact, if the definition of writeLine is commented out, the program typechecks! It gets weirder: if the definition of writeLine is moved in between the definitions of readFile and writeFile, then the unexpected error is reported for the definition of readFile, and if writeLine is moved above both of them, then the error isn’t reported at all!

This implies that a well-typed function (writeFile) can actually become ill-typed after the addition of an unrelated, ill-typed definition (writeLine). That seems like a bug to me.

I was able to reproduce this issue on GHC 7.10.3, 8.0.2, and 8.2.1.

Change History (4)

comment:1 Changed 2 years ago by dfeuer

Even weirder: when I added the definitions of the relevant functions and classes from Control.Monad.Free to the test module (to remove the dependency on free), I found that the problem is now sensitive to the definition order in a different way.

{-# language DeriveFunctor, FunctionalDependencies
      , MultiParamTypeClasses, FlexibleInstances #-}
module T14327 where
import Prelude hiding (readFile, writeFile)
import Data.Functor.Sum

data Free f a = Pure a | Free (f (Free f a)) deriving (Functor)

class Monad m => MonadFree f m | m -> f where
  wrap :: f (m a) -> m a

instance MonadFree f (Free f) where
  wrap = Free

liftF :: (Functor f, MonadFree f m) => f a -> m a
liftF fa = wrap (return <$> fa)

data FileSystemF a
  = ReadFile FilePath (String -> a)
  | WriteFile FilePath String a
  deriving (Functor)

data ConsoleF a
  = WriteLine String a
  deriving (Functor)

data CloudF a
  = GetStackInfo String (String -> a)
  deriving (Functor)

type App = Free (Sum FileSystemF (Sum ConsoleF CloudF))

The surprising error does not occur with the three functions defined in their original order, but it does occur if writeLine appears before at least one of the other definitions.

comment:2 Changed 2 years ago by dfeuer

Cc: dfeuer added
Milestone: 8.4.1

comment:3 Changed 2 years ago by RyanGlScott

I'm a bit confused here. The program in comment:1 is incomplete, and it's not clear to me where you put writeLine and friends after the fact. Can you post the complete version of the programs you're running, with and without the reordering of writeLine?

comment:4 Changed 2 years ago by RyanGlScott

Keywords: FunDeps added
Resolution: duplicate
Status: newclosed

OK, it turns out this is actually a duplicate of #13506. First, here is the program that I tested, for the sake of posterity:

{-# language DeriveFunctor, FunctionalDependencies
      , MultiParamTypeClasses, FlexibleInstances #-}
module T14327 where
import Prelude hiding (readFile, writeFile)
import Data.Functor.Sum

data Free f a = Pure a | Free (f (Free f a)) deriving (Functor)

class Monad m => MonadFree f m | m -> f where
  wrap :: f (m a) -> m a

instance Functor f => Applicative (Free f)
instance Functor f => Monad (Free f)

instance Functor f => MonadFree f (Free f) where
  wrap = Free

liftF :: (Functor f, MonadFree f m) => f a -> m a
liftF fa = wrap (return <$> fa)

data FileSystemF a
  = ReadFile FilePath (String -> a)
  | WriteFile FilePath String a
  deriving (Functor)

data ConsoleF a
  = WriteLine String a
  deriving (Functor)

data CloudF a
  = GetStackInfo String (String -> a)
  deriving (Functor)

type App = Free (Sum FileSystemF (Sum ConsoleF CloudF))

writeLine :: String -> App ()
writeLine line = liftF (InR (WriteLine line ()))

readFile :: FilePath -> App String
readFile path = liftF (InL (ReadFile path id))

writeFile :: FilePath -> String -> App ()
writeFile path contents = liftF (InL (WriteFile path contents ()))

On GHC 8.2.1 and earlier, this does indeed spuriously give more errors than it should:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling T14327           ( /u/rgscott/Documents/Hacking/Haskell/Bug.hs, interpreted )

/u/rgscott/Documents/Hacking/Haskell/Bug.hs:37:18: error:
    • Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’
        arising from a functional dependency between:
          constraint ‘MonadFree
                        (Sum FileSystemF ConsoleF)
                        (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’
          instance ‘MonadFree f (Free f)’
            at /u/rgscott/Documents/Hacking/Haskell/Bug.hs:15:10-42
    • In the expression: liftF (InR (WriteLine line ()))
      In an equation for ‘writeLine’:
          writeLine line = liftF (InR (WriteLine line ()))
   |
37 | writeLine line = liftF (InR (WriteLine line ()))
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

/u/rgscott/Documents/Hacking/Haskell/Bug.hs:40:17: error:
    • Couldn't match type ‘ConsoleF’ with ‘Sum ConsoleF CloudF’
        arising from a functional dependency between constraints:
          ‘MonadFree
             (Sum FileSystemF (Sum ConsoleF CloudF))
             (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’
            at /u/rgscott/Documents/Hacking/Haskell/Bug.hs:40:17-46
          ‘MonadFree
             (Sum FileSystemF ConsoleF)
             (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’
            at /u/rgscott/Documents/Hacking/Haskell/Bug.hs:37:18-48
    • In the expression: liftF (InL (ReadFile path id))
      In an equation for ‘readFile’:
          readFile path = liftF (InL (ReadFile path id))
   |
40 | readFile path = liftF (InL (ReadFile path id))
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

But on GHC HEAD, it doesn't!

GHCi, version 8.3.20171004: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling T14327           ( /u/rgscott/Documents/Hacking/Haskell/Bug.hs, interpreted )

/u/rgscott/Documents/Hacking/Haskell/Bug.hs:37:18: error:
    • Couldn't match type ‘Sum ConsoleF CloudF’ with ‘ConsoleF’
        arising from a functional dependency between:
          constraint ‘MonadFree
                        (Sum FileSystemF ConsoleF)
                        (Free (Sum FileSystemF (Sum ConsoleF CloudF)))’
            arising from a use of ‘liftF’
          instance ‘MonadFree f (Free f)’
            at /u/rgscott/Documents/Hacking/Haskell/Bug.hs:15:10-42
    • In the expression: liftF (InR (WriteLine line ()))
      In an equation for ‘writeLine’:
          writeLine line = liftF (InR (WriteLine line ()))
   |
37 | writeLine line = liftF (InR (WriteLine line ()))
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It turns out that commit 48daaaf0bba279b6e362ee5c632de69ed31ab65d (Don't report fundep wanted/wanted errors) fixed this problem. This led me to realize that this entire ticket is simply a more involved version of the program in #13506 (which concerns error cascades with functional dependencies), the ticket that the aforementioned commit originally fixed. So I'll close this as a duplicate.

Note: See TracTickets for help on using tickets.