Unspecified skolem error on some pretty basic code

[prescientmoon]

Description

The compiler fails with an internal error on some pretty basic code.

purs: An internal error occurred during compilation: unifyTypes: unspecified skolem scope
Please report this at https://github.com/purescript/purescript/issues
CallStack (from HasCallStack):
  error, called at src/Language/PureScript/Crash.hs:10:3 in purescript-0.15.8-CpwrQDGmzs8DpDoZbblmgT:Language.PureScript.Crash
  internalError, called at src/Language/PureScript/TypeChecker/Unify.hs:124:12 in purescript-0.15.8-CpwrQDGmzs8DpDoZbblmgT:Language.PureScript.TypeChecker.Unify

To Reproduce

Compile the following:

module Control.Monad.State.External where

import Prelude

import Control.Monad.Reader (ReaderT(..))
import Control.Monad.State (class MonadState)
import Data.Tuple.Nested (type (/\), (/\))

type ExternalStateContext s m = forall a. (s -> a /\ s) -> m a

newtype ExternalStateT s m a = ExternalStateT (ReaderT (ExternalStateContext s m) m a)

derive newtype instance Functor m => Functor (ExternalStateT s m)
derive newtype instance Apply m => Apply (ExternalStateT s m)
derive newtype instance Applicative m => Applicative (ExternalStateT s m)
derive newtype instance Bind m => Bind (ExternalStateT s m)
derive newtype instance Monad m => Monad (ExternalStateT s m)
instance Monad m => MonadState s (ExternalStateT s m) where
  state f = ExternalStateT $ ReaderT 
    \(mkState :: ExternalStateContext s m) -> mkState f

PureScript version

0.15.8

[prescientmoon]

Could be related perhaps? #3681

[klarkc]

Could be related perhaps? #3681

@mateiadrielrafael from GPT:

Yes, the errors you're encountering are related. The issue seems to be related to the use of an existential quantification (forall) with a type synonym (type) in the Inhabitant type class in the first code example (their), and the type synonym ExternalStateContext in the second code example (yours).

In PureScript, type synonyms are expanded during compilation, and if the resulting type is ill-formed or has issues with skolem scopes (which are used to handle quantified types), it can lead to compilation errors like the ones you're encountering.

To test the existential substitution in your code, you can try substituting the type synonyms directly in the instances or function signatures where they are used, and see if the code compiles without any errors. For example, in the first code example, you can try replacing the Inhabitant type class instance with the expanded version of the type synonym Inhabitant:

instance inhabits :: (Cons k s x adt, Extract s (forall x. Inhabits adt x => x) v) => Inhabits adt { label :: SProxy k, value :: v }

Similarly, in the second code example, you can replace the ExternalStateContext type synonym with its expanded version:

newtype ExternalStateT s m a = ExternalStateT (ReaderT ((forall a. (s -> a /\ s) -> m a)) m a)

By doing so, you can check if the code compiles without any issues related to skolem scopes or existential quantifications. If the code compiles without any errors, it may indicate that the issue is related to the use of type synonyms in combination with existential quantifications.

It makes sense, I guess.

[prescientmoon]

The code does work when turning the type alias into a newtype.

[garyb]

Regardless of whether the code should work without annotations (I think this would count as impredicative), it shouldn't be reaching that crash case so +1 for it being a bug.