Skip to content

Existential scope escape using variable name #502

Description

@Bowuigi
{-# LANGUAGE BlockArguments #-}
module Main where

import Data.STRef
import Control.Monad.ST

data Ex where
  Ex :: STRef r Int -> Ex

-- Pack `STRef s Int` into an existential, hiding the value of `s` (and Int but that's irrelevant)
ok :: Ex
ok = runST do
  ref <- newSTRef 1
  return (Ex ref)

-- Precisely what shouldn't happen
-- Do note that if I rename `r` to `s` it signals a (correct) error
-- (∃r. STRef r Int) -> (∀r. STRef r Int)
wrong :: Ex -> forall r. STRef r Int
wrong (Ex ref) = ref

-- Same here: Renaming r to s signals a (correct) error
wrong2 :: Ex -> forall r. ST r Int
wrong2 (Ex ref) = readSTRef ref

main = putStrLn "Hello!"

Renaming r to s signals this error (correct behavior):

*** Exception: error: "./Main.hs": line 21, col 18: Cannot satisfy constraint: r ~ s
     fully qualified: Primitives.~ r s

GHC raises this error when loading the original version:

Main.hs:21:18: error: [GHC-25897]
    • Couldn't match type ‘r1’ with ‘r’
      Expected: STRef r Int
        Actual: STRef r1 Int
      ‘r1’ is a rigid type variable bound by
        a pattern with constructor: Ex :: forall r. STRef r Int -> Ex,
        in an equation for ‘wrong’
        at Main.hs:21:8-13
      ‘r’ is a rigid type variable bound by
        the type signature for:
          wrong :: Ex -> forall r. STRef r Int
        at Main.hs:21:1-20
    • In the expression: ref
      In an equation for ‘wrong’: wrong (Ex ref) = ref
    • Relevant bindings include
        ref :: STRef r1 Int (bound at Main.hs:21:11)
   |
21 | wrong (Ex ref) = ref
   |                  ^^^

(And then another one for wrong2 but it's basically the same error)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions