Type system troubles: RankNTypes Typeclasses-CodePudding

I've been having some troubles with combining typeclasses with higher-rank types in haskell.

The project I'm working on is an interpreter based around an evaluation monad. I'm currently attempting to transition my central evaluation monad from a stack of transformers to a set of mtl constraints. Many of the functions I'm using have type signatures like:

(MonadReader Environment m, MonadError String m, MonadState ProgState m) => <something involving m>

In addition, I'm placing higher-rank polymorphic functions inside of some datastructures, e.g.

data Foo = 
  ...
  | forall m. MonadReader Environment m, ..., ... => <something involving m>

I've been using several language extensions, but I think the relevant ones are {-# LANGUAGE RankNTypes, FlexibleContexts #-}.

As part of this transition, I'm running into two type errors throughout the codebase, but there's one snippet which demonstrates both (below).

At the surface level, it'd be nice if I can fix these issues, but I feel that all these type errors are related to my lack of understanding of how higher-rank types in Haskell work, so if there are any papers or articles that you feel may help they'd be much appreciated.

The Problem

The below snippet demonstrates both type-errors I'm getting:

normSubst :: (MonadReader Environment m, MonadError String m, MonadState ProgState m) => (Normal, String) -> Normal -> m Normal
normSubst (val, var) ty = case ty of 
  -- ...
  NormCoVal pats ty -> do
    let pats' = map substCoPat pats
    ty' <- normSubst (val, var) ty
    pure (NormCoVal pats' ty')

Relevant type signatures include:

data Normal = 
 ...
 | NormCoVal (forall m. (MonadReader Environment m, MonadError String m, MonadState ProgState m) => [(CoPattern, m Normal)]) Normal


substCoPat :: (MonadReader Environment m, MonadError String m, MonadState ProgState m) => (CoPattern, m Normal) -> (CoPattern, m Normal)

Error 1

This error seems to be related to the line let pats' = map substCoPat pats, and has occurred a couple times. Several of these seem related to uses of combinators from the Lens library.

error:
    • Could not deduce (MonadReader Environment m0)
        arising from a use of ‘substCoPat’
      from the context: (MonadReader Environment m, MonadError String m,
                         MonadState ProgState m)
        bound by the type signature for:
                   normSubst :: forall (m :: * -> *).
                                (MonadReader Environment m, MonadError String m,
                                 MonadState ProgState m) =>
                                (Normal, String) -> Normal -> m Normal
        at src/Interpret/Eval.hs:386:1-128
      The type variable ‘m0’ is ambiguous
      Relevant bindings include
        pats' :: [(CoPattern, m0 Normal)]

Error 2

This error is related to the line pure (NormCoVal pats' ty'), specifically the pats variable. I've found something relating to this second error here, but can't quite make sense of what the article is saying.

error:
    • Couldn't match type ‘m0’ with ‘m1’
      Expected: [(CoPattern, m1 Normal)]
        Actual: [(CoPattern, m0 Normal)]
        because type variable ‘m1’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          forall (m1 :: * -> *).
          (MonadReader Environment m1, MonadError String m1,
           MonadState ProgState m1) =>
          [(CoPattern, m1 Normal)]

CodePudding user response：

I think the usual advice of "do not try to store type classes inside data types" applies in this case.

You can restructure your program like this:

normSubst :: 
  ( MonadReader Environment m
  , MonadError String m
  , MonadState ProgState m
  ) => (Normal m, String) -> Normal m -> m (Normal m)
normSubst (val, var) ty = case ty of 
  -- ...
  NormCoVal pats ty -> do
    let pats' = map substCoPat pats
    ty' <- normSubst (val, var) ty
    pure (NormCoVal pats' ty')

data Normal m = 
 ...
 | NormCoVal [(CoPattern, m (Normal m))] (Normal m)


substCoPat :: 
  ( MonadReader Environment m
  , MonadError String m
  , MonadState ProgState m
  ) => (CoPattern, m (Normal m)) -> (CoPattern, m (Normal m))

CodePudding user response：

In this example, these errors are caused by the monomorphism restriction. It causes pats' to be assumed monomorphic for some unspecified monad m0. In order to call substCoPat at this type, GHC goes looking for appropriate dictionaries for m0, which are nowhere to be found (Error 1). And the use of pats' on the last line is too monomorphic. It only works for that ambiguous monad m0, but you're using it in a context where in needs to work forall m1. (...constraints...) => ... for some fresh m1 type variable (Error 2).

Just turn off the restriction with the {-# LANGUAGE NoMonomorphismRestricition #-}, and a proper polymorphic type for pats' will be inferred.

Alternatively, adding an explicit type signature:

  NormCoVal pats ty -> do
    let pats' :: (MonadReader Environment m, MonadError String m, MonadState ProgState m) => [(CoPattern, m Normal)]
        pats' = map substCoPat pats
    ty' <- normSubst (val, var) ty
    pure (NormCoVal pats' ty')

or avoiding the let:

  NormCoVal pats ty -> do
    ty' <- normSubst (val, var) ty
    pure (NormCoVal (map substCoPat pats) ty')

would work, too.