Type error in program caused by unrelated definition
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 |