GitLab

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.

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture