Compiler panic when unifying inner skolem with an outer unification variable

[Innf107]

Quick Summary: The compiler crashes in compiler/src/Type/Solve.hs:206:15 when checking the body of g, which unifies a skolem bound in the type of g (a) with a unification variable from the definition of f (the type of x)

SSCCE

f x = let g : (a -> ()) -> ()
          g h = h x
      in x

• Elm: 1.19.1
• Browser: N/A
• Operating System: Linux x86-64

Additional Details

This should result in an error, ideally with a nice error message. The reason I even found this is that the error messages reported by both GHC and OCaml are quite poor.

Error message

Compiling ...elm: You ran into a compiler bug. Here are some details for the developers:

    a [rank = 2]

Please create an <http://sscce.org/> and then report it
at <https://github.com/elm/compiler/issues>


CallStack (from HasCallStack):
  error, called at compiler/src/Type/Solve.hs:206:15 in main:Type.Solve

-- ERROR -----------------------------------------------------------------------

I ran into something that bypassed the normal error reporting process! I
extracted whatever information I could from the internal error:

>   thread blocked indefinitely in an MVar operation

These errors are usually pretty confusing, so start by asking around on one of
forums listed at https://elm-lang.org/community to see if anyone can get you
unstuck quickly.

-- REQUEST ---------------------------------------------------------------------

If you are feeling up to it, please try to get your code down to the smallest
version that still triggers this message. Ideally in a single Main.elm and
elm.json file.

From there open a NEW issue at https://github.com/elm/compiler/issues with your
reduced example pasted in directly. (Not a link to a repo or gist!) Do not worry
about if someone else saw something similar. More examples is better!

This kind of error is usually tied up in larger architectural choices that are
hard to change, so even when we have a couple good examples, it can take some
time to resolve in a solid way.elm: thread blocked indefinitely in an MVar operation

[github-actions[bot]]

Thanks for reporting this! To set expectations:

• Issues are reviewed in batches, so it can take some time to get a response.
• Ask questions in a community forum. You will get an answer quicker that way!
• If you experience something similar, open a new issue. We like duplicates.

Finally, please be patient with the core team. They are trying their best with limited resources.

[lue-bird]

If you need a quick fix, try adding a type annotation to the module-level declaration. Issue seems similar to https://github.com/elm/compiler/issues/1839

[mheiber]

Re

The reason I even found this is that the error messages reported by both GHC and OCaml are quite poor.

What's the OCaml error message? This OCaml translation compiles and runs on at least OCaml 4.13.1 and 5.0.0:

let f x =
  let _g : (('a -> unit) -> unit) = fun h -> h x
  in x

https://try.ocamlpro.com/#code/let'f'x'=!let'_g':'(($,a'-$.'unit)'-$.'unit)'='fun'h'-$.'h'x!in'x

[Innf107]

This is quite subtle, but the OCaml type you wrote is not actually equivalent to the one in Elm.

'a variables are not implicitly quantified type variables like in Elm or Haskell. They are actually just stand-ins for unification variables, which are closer to _a with PartialTypeSignatures in Haskell. In other words, the following will compile and define a function f : Int -> int

let f : 'a -> 'a = fun x -> x + 1

To get the fully polymorphic behavior like in Elm or Haskell, one needs to use an explicit quantifier

let f x =
     let g : 'a. ('a -> unit) -> unit =
         fun h -> h x
     in x

This generates the "fantastic" error message

Error: This definition has type ('a -> unit) -> unit which is less general than
         'a0. ('a0 -> unit) -> unit