[GHC] #14327: Type error in program caused by unrelated definition

5 Oct 2017

      #14327: Type error in program caused by unrelated definition
-------------------------------------+-------------------------------------
           Reporter:  lexi.lambda    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 ''Adapted from [https://stackoverflow.com/q/46595162/465378 this Stack
 Overflow question].''

 The following program raises two type errors:

 {{{#!hs
 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14327
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler