Issue with synonym expansion in superclass constraints

[drewolson]

In this example, I've implemented the MonadThrow and MonadAsk type classes for a newtype called App. The config provided by my MonadAsk is a record. Because of the restriction on aliases in type classes, I must use TypeEquals to define this instance.

Once defined, I can interpret function with the MonadAsk Env m constraint with my App type (see doStuff), but if I try to constrain a function with the same MonadAsk Env m in a type class alias, it no longer works (see doStuffA and doStuffB). I think this may be a bug with the type checker.

[hdgarrood]

Can you please include the errors you're getting?

[garyb]

I suspect it's to do with not using TE.from / TE.to as necessary to get the instances to work. You can't ever assume the type being asked for is Env, it'll always need the coercion too.

[garyb]

I'd suggest newtyping Env, and then providing an askEnv :: MonadAsk Env m => m { ... } function that unwraps the record, rather than using TypeEquals for this sort of thing, by the way.

[drewolson]

@hdgarrood Apologies, my error is below[1].

@garyb I agree, and in my real application I did end up newtypeing Env. But the fact that the code compiles with a direct constraint of MonadAsk Env m but fails with a type class alias of the same type seems strange.

[1]

in module Main
at src/Main.purs:62:14 - 62:17 (line 62, column 14 - line 62, column 17)

  Could not match type
      
    r4
      
  with type
                   
    { foo :: String
    | t2           
    }              
                   

while solving type class constraint
                                                     
  Control.Monad.Reader.Class.MonadAsk { foo :: String
                                      | t2           
                                      }              
                                      m3             
                                                     
while checking that type forall m r. MonadAsk r m => m r
  is at least as general as type t0 t1
while checking that expression ask
  has type t0 t1
in value declaration doStuffB

where m3 is a rigid type variable
        bound at (line 61, column 12 - line 66, column 26)
      r4 is a rigid type variable
        bound at (line 61, column 12 - line 66, column 26)
      t0 is an unknown type
      t1 is an unknown type
      t2 is an unknown type

See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
or to contribute content related to this error.


spago: Failed to build.```

[garyb]

Yeah, that error is definitely due to a lack of to or from somewhere: it's trying to unify r with Env, where r was the variable you used for the TypeEquals.

[drewolson]

@garyb just to make sure I'm being clear, the following code[1] does compile. It only fails if I use a type class alias to provide the same constraint.

[1]

import Prelude

import Control.Monad.Error.Class (class MonadThrow, throwError)
import Control.Monad.Except (ExceptT, runExceptT)
import Control.Monad.Reader (class MonadAsk, ReaderT, ask, runReaderT)
import Data.Either (Either)
import Effect (Effect)
import Effect.Aff (Aff, launchAff_)
import Effect.Class.Console as Console
import Type.Equality (class TypeEquals)
import Type.Equality as TE

type Env =
  { foo :: String
  }

newtype App a = App (ExceptT String (ReaderT Env Aff) a)

derive newtype instance functorApp :: Functor App

derive newtype instance applyApp :: Apply App

derive newtype instance applicativeApp :: Applicative App

derive newtype instance bindApp :: Bind App

derive newtype instance monadApp :: Monad App

derive newtype instance monadThrow :: MonadThrow String App

instance monadAskApp :: TypeEquals Env r => MonadAsk r App where
  ask :: App r
  ask = App (TE.to <$> ask)

-- compiles fine
doStuff :: forall m. MonadThrow String m => MonadAsk Env m => m String
doStuff = do
  { foo } <- ask

  if foo == "hi"
    then throwError "boom"
    else pure "greetings"

runApp :: forall a. App a -> Aff (Either String a)
runApp (App app) = runReaderT (runExceptT app) { foo: "hello" }

main :: Effect Unit
main = launchAff_ do
  result <- runApp doStuff
  Console.logShow result

[hdgarrood]

Yes, that's expected. doStuffB should definitely fail with an error like that. The reason for this is that TypeEquals has no special compiler support, unlike Haskell's ~, so the compiler cannot deduce MonadAsk Env m given TypeEquals Env r and MonadAsk r m.

What do you get if you take that example and only remove doStuffB? Does doStuffA still fail? If so, that may be a bug.

[drewolson]

@hdgarrood doStuffA in isolation does indeed fail. Here's the code[1] and error[2].

[1]

import Prelude

import Control.Monad.Error.Class (class MonadThrow, throwError)
import Control.Monad.Except (ExceptT, runExceptT)
import Control.Monad.Reader (class MonadAsk, ReaderT, ask, runReaderT)
import Data.Either (Either)
import Effect (Effect)
import Effect.Aff (Aff, launchAff_)
import Effect.Class.Console as Console
import Type.Equality (class TypeEquals)
import Type.Equality as TE

type Env =
  { foo :: String
  }

newtype App a = App (ExceptT String (ReaderT Env Aff) a)

derive newtype instance functorApp :: Functor App

derive newtype instance applyApp :: Apply App

derive newtype instance applicativeApp :: Applicative App

derive newtype instance bindApp :: Bind App

derive newtype instance monadApp :: Monad App

derive newtype instance monadThrow :: MonadThrow String App

instance monadAskApp :: TypeEquals Env r => MonadAsk r App where
  ask :: App r
  ask = App (TE.to <$> ask)

class (MonadThrow String m, MonadAsk Env m) <= MonadApp m

doStuffA :: forall m. MonadApp m => m String
doStuffA = do
  { foo } <- ask

  if foo == "hi"
    then throwError "boom"
    else pure "greetings"

runApp :: forall a. App a -> Aff (Either String a)
runApp (App app) = runReaderT (runExceptT app) { foo: "hello" }

main :: Effect Unit
main = launchAff_ do
  result <- runApp doStuffA
  Console.logShow result

[2]

in module Main
at src/Main.purs:41:14 - 41:17 (line 41, column 14 - line 41, column 17)

  Could not match type
       
    Env
       
  with type
                   
    { foo :: String
    | t2           
    }              
                   

while solving type class constraint
                                                     
  Control.Monad.Reader.Class.MonadAsk { foo :: String
                                      | t2           
                                      }              
                                      m3             
                                                     
while checking that type forall m r. MonadAsk r m => m r
  is at least as general as type t0 t1
while checking that expression ask
  has type t0 t1
in value declaration doStuffA

where m3 is a rigid type variable
        bound at (line 40, column 12 - line 45, column 26)
      t0 is an unknown type
      t1 is an unknown type
      t2 is an unknown type

See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
or to contribute content related to this error.


spago: Failed to build.```

[garyb]

👍

Looks like the Env synonym fails to expand / be substituted in that situation. Another thing that'll need fixing for #3539 then.

[hdgarrood]

Thanks! Minimal repro:

module Main where
import Prelude

type Env = { foo :: String }

class (Monad m, MonadAsk Env m) <= MonadAskEnv m

test :: forall m. MonadAskEnv m => m Boolean
test = do
  { foo } <- ask
  pure (foo == "test")

fails with:

  
  Could not match type
  
    Env
  
  with type
  
    { foo :: String
    | t2
    }
  
  while solving type class constraint
  
    Main.MonadAsk { foo :: String
                  | t2
                  }
                  m3