Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,273
    • Issues 4,273
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 413
    • Merge Requests 413
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14327

Closed
Open
Opened Oct 05, 2017 by Alexis King@lexi.lambda

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
Assignee
Assign to
8.4.1
Milestone
8.4.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#14327