Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,867
    • Issues 4,867
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #21309
Closed
Open
Created Mar 28, 2022 by Richard Eisenberg@raeDeveloper

Order dependence in type checking with the monomorphism restriction

The order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes, though, a constraint can be eagerly solved, making it disappear (and thus not affecting any variables).

A nested example:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where

class C a b where
  method :: a -> b -> ()
instance C Char b where
  method _ _ = ()
f1 x = let g = \y -> method x y in
       (x : "hi", (g True, g Nothing))

f2 x = (x : "hi",
        let g = \y -> method x y in
        (g True, g Nothing))

f1 is rejected, as method x y gives rise to [W] C alpha beta, which cannot be solved. Then, g is not generalised, so we get g :: beta -> (), which is not general enough for its two usages.

f2 is accepted, as method x y gives rise to [W] C Char beta, easily solved by the instance. No MR happens.

A top-level example:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug2 where

x = 5

class C a b where
  method :: a -> b -> ()
instance C Int b where
  method _ _ = ()

x2 :: (Int, ((), ()))
x2 = (x + 1, (g True, g 'x'))  -- remove references to 'g' to allow module to be accepted

g = \y -> method x y

x3 :: ((), ())
x3 = (g True, g 'x')

This is rejected. Note that x2 depends on g, and thus g is type-checked first -- critically, before we know that x :: Int. So the MR kicks in and prevents generalisation. However if we change to x2 = (x + 1, ((), ())), then the module is accepted: x2 gets seen first, we learn that x :: Int, and then there is no constraint to prevent generalisation in g. The two different uses in x3 are accepted.

I don't think this will be easy to fix: we would somehow need to delay the computation of whether or not to generalise, and that seems Very Hard. Maybe this just gets filed in the user manual under FlexibleInstances and how flexibility can sometimes cause trouble? Not sure. Note that "let should not be generalised" is not enough here, because the problem can manifest at top-level.

This is based on a conversation with @simonpj this morning; credit to him for outlining the problem.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking