infinite type inferred due to pattern variable

Question

Using a pattern variable that names an entire case expression makes the difference between compiling correctly and the error "An infinite type was inferred for an expression". The following compiles correctly:

m = case Left "anything" of
  e@(Left err) -> Left err
  (Right f) -> case lookup "key" f of
    Nothing -> Left "something else"
    (Just x) -> Right x

However, if we use the pattern variable e (substituting e for "Left err", functionally equivalent), the compiler flags an error:

m = case Left "anything" of
  e@(Left err) -> e
  (Right f) -> case lookup "key" f of
    Nothing -> Left "something else"
    (Just x) -> Right x

"An infinite type was inferred for an expression: StrMap t1 while trying to match type t1 with type StrMap t1 while checking that expression case ((lookup "key") f) ...

I understand that matching StrMap t1 with t1 is problematic. I do not understand why this happens. Also, in my original code the message did not refer to infinite types at all. Here is the relevant extract:

retrieveDomeinResourceDefinition :: forall e.
  ResourceId
  -> Namespace
  -> (AsyncDomeinFile e (Either String PropDefs))
retrieveDomeinResourceDefinition id ns = do
  df <- retrieveDomeinFile (namespaceToDomeinFileName ns)
  case df of
    e@(Left err) -> pure $ e
    (Right f) -> case lookup id f of
      Nothing -> pure $ Left ("retrieveDomeinResourceDefinition: cannot find definition of " <> id <> " in DomeinFile for " <> ns)
      (Just propDefs) -> pure (Right propDefs)

retrieveDomeinFile :: forall e. Namespace -> AsyncDomeinFile e (Either String DomeinFile)

newtype PropDefs = PropDefs (StrMap Json)

Now here the compiler tells me: "Could not match type: PropDefs with type StrMap PropDefs..." It appears as if the compiler does not notice the lookup expression. In fact, when I replace "pure (Right propDefs)" with "pure (Right f)", the error goes away (and another appears on the line binding df, which I understand).

Now I write this up I notice the similarity between 'trying to match type t1 with type StrMap t1' and 'could not match type: PropDefs with StrMap PropDefs'. Still, I don't see why using e introduces this problem.

gb. gb. · Accepted Answer · 2017-08-09T15:19:41

Using the value from a pattern match that way may be functionally equivalent, but the types are not - the type system doesn't have the evidence that the type variable for the Right can be ignored.

Using the types in your second example - when you pattern match e@(Left err), the type of e will be Either String DomeinFile - but you want an Either String PropDefs. The pattern match does not "free up" the type variable on the right, which is why you have to reconstruct the Left with the error again.

infinite type inferred due to pattern variable

1 Answers