I am getting an error message like so:
Linear.hs:215:27:
Couldn't match expected type `forall v1.
Ident v1 =>
SubstT v1 (GenericLL (a v1 c)) n x'
with actual type `forall v1. Ident v1 => SubstT v1 a0 m0 b0'
Expected type: (forall v1.
Ident v1 =>
SubstT v1 (GenericLL (a v1 c)) n x)
-> n x
Actual type: (forall v1. Ident v1 => SubstT v1 a0 m0 b0) -> m0 b0
In the first argument of `flattenImpl', namely `runSubstT'
In the expression: flattenImpl runSubstT
The actual type seems more general than the expected type. What are then possible causes for this kind of error message? Is the message misleading or am I reading it incorrectly?
What I am trying to do is to pass an existentially quantified function runSubstT
, whose type is:
runSubstT :: (Monad m) => (forall v. (Ident v) => SubstT v a m b) -> m b
I will also settle with some good description of how the GHC compiler performs type matching on existentially quantified types.
I have a guess, but I cannot be sure until you post enough code to reproduce the error. My guess, based on looking at this:
runSubstT :: (Monad m) => (forall v. (Ident v) => SubstT v a m b) -> m b
is that making the second type 'a' dependent on the first existential type 'v' may be a problem. The expected type:
forall v1. Ident v1 => SubstT v1 (GenericLL (a v1 c)) n x'
replaces the second type with (GenericLL (a v1 c)) which depends on the first existential type 'v1'. This could be the root of the conflict, but without the code I cannot trace the login of the type checker.