Type variable has escaped it's scope after deconstruction

#1

Hi,

i’m struggling to understand the compiler regarding type synonyms. Can someone please explain to me if this is a bug or intended behavior.

module Main where

import Prelude

type Make m = {
  make :: forall x . m x
}

type Context m r = {
  bm :: Make m | r
}

test :: forall m r. (Monad m) => Context m r -> m Unit
test ctx = do
  -- works fine
  _ <- ctx.bm.make
  -- bm seems to have a different type after deconstruction because this fails to compile
  let { bm } = ctx
  _ <- bm.make
  -- this again works
  let { bm: bm' :: Make m } = ctx
  _ <- bm'.make
  -- this works too
  let { bm: bm'' :: { make :: forall x . m x }} = ctx
  _ <- bm''.make
  pure unit

The error is:

  The type variable x, bound at

    <file>:6:11 - 6:25 (line 6, column 11 - line 6, column 25)

  has escaped its scope, appearing in the type

    (x2 -> m1 Unit) -> m1 Unit


in the expression (bind (($dictMonad0."Bind1") undefined)) (bm.make)
in value declaration test

see: https://try.purescript.org/?session=ba69099e-3474-95fe-8e4e-41a8c54f5a07

I find it very hard to debug those kind of unification problems in a larger context.

Thx a lot,
Heinz

#2

Unexpected things happening when putting higher rank types in records is a common theme in the PS issue tracker. Often there is a sensible explanation for it, even if it’s undesired in a particular use case, but there probably are some bugs too. This is perhaps https://github.com/purescript/purescript/issues/3749 ?

Using data constructors or newtyping the records can make it a bit more predictable.

Newtyping helps because it can direct the quantification better, since for this record, there are several ways it could be treated, all with different meanings:

forall m x. { make :: m x }
forall m. { make :: forall x. m x }
{ make :: forall m x. m x }
#3

Ah, thx for the heads-up, i will watch the issue then :wink: