Alexis King
Alexis King

Reputation: 43842

Why do I get a type error in this program when I add an unrelated definition?

I was showing a coworker Free when I ran into a curious GHC behavior I don’t really understand. Here is a simple, contrived program that typechecks:

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 ()))

I tried adding another definition, but it wasn’t quite right:

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

The problem here is that I was missing another InL. The correct definition should be this:

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

However, that isn’t the point. What’s weird to me is the type error that GHC produced when I added my first, incorrect definition of writeLine. Specifically, it produced two type errors:

/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. But the error on line 26 completely baffles me. The definition of writeFile is correct! Adding my incorrect definition of writeLine shouldn’t have any effect on writeFile, right? What’s going on?

I was able to reproduce this on GHC 8.0.2 and GHC 8.2.1. I’d like to know if this is a bug in GHC (so I can report it) or if it’s an issue with my code that I don’t understand.

Upvotes: 12

Views: 140

Answers (1)

dfeuer
dfeuer

Reputation: 48591

This was a GHC bug. It was fixed in commit 48daaaf0bba279b6e362ee5c632de69ed31ab65d (Don't report fundep wanted/wanted errors), according to Ryan Scott.

Upvotes: 8

Related Questions