Inferred generic function typechecks as a return type but not an argument type

Question

I'm learning about SYB and rank n types, and came across a confusing case of what seems like the monomorphism restriction.

I wrote a function to find the shallowest entry that matches a predicate. Instead of a reducing function, I wanted to accept a more predicate-like function using Alternative, and transform it into a generic function myself. I decided to omit the type annotation in the let block to see how the monomorphism reduction would affect the type in this implementation:

shallowest :: (Alternative f, Typeable b) => (b -> f a) -> GenericQ (f a)
shallowest p z =
  let op = (empty `mkQ` p) in
    op z <|> foldl (<|>) empty (gmapQ op z)

This produces an error that suggests that the ambiguity in the let binding prevents the typechecker from solving the constraint Data a1.

Error: • Couldn't match type ‘d’ with ‘a1’
  ‘d’ is a rigid type variable bound by
    a type expected by the context:
      forall d. Data d => d -> m a
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      shallowest :: (b -> m a) -> GenericQ (m a)

(Other bodies like head (gmapQ op z) cause an explicit error about ambiguity for the let binding along the lines of "Could not deduce (Typeable a0) arising from a use of ‘mkQ’"; I also haven't figured out why the above form doesn't).

The type error goes away when we add an annotation in the let block for op :: GenericQ (f a) (requiring ScopedTypeVariables).

However, I'm confused that it seems the Data constraint on op can be inferred: the follow typechecks when it's the return type:

shallowest p = let { op = (empty `mkQ` p) } in op

What's the difference? Both cases require op to be forall d. Data d => d -> f a; the only difference I see is that the first is in an argument position and the second is in a return position.

Li-yao Xia Li-yao Xia · Accepted Answer · 2019-05-26T17:33:49

In your second snippet, op is actually not polymorphic.

shallowest p = let { op = (empty `mkQ` p) } in op

It is a subtle difference: op is in fact monomorphic, but in an open context. With the usual notation for typing judgements, the typing of op to the right of in looks as follows:

 types         values
 ↓             ↓
 x, a, f, ...; op :: x -> f a, ... |- op :: x -> f a
                                            ↑
                                            monotype (no "forall")

 In English: "op has type (x -> f a) in the context consisting of type variables (x, a, f, ...) and values (op :: x -> f a, ...)"

shallowest is made polymorphic by a generalization step that happens at the toplevel. If, in a context with type variables x, a, f, ..., the body of shallowest has type x -> f a, then we can "close the context" and move the type variables into the type of shallowest :: forall x a f. x -> f a. The type derivation looks like this:

     x, a, f |- (let op = ... in op) :: x -> f a
 ⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻ (generalization)
   |- (let op = .... in op) :: forall x a f. x -> f a

(Things are complicated further by type classes and unification algorithms, but that's beside the point of this answer.)

The main problem for typechecking with polymorphism is to decide when generalization should happen. There is no general solution, by lack of principal types and by undecidability. So a typechecker implementation has to make some choices.

In Haskell, generalization happens at the following locations (the list might not be exhaustive), which are fairly natural choices:

function definitions, i.e., let and toplevel bindings with at least one explicit argument (here is the monomorphism restriction);
polymorphic arguments of higher-rank functions: if you have a function f :: (forall a. w a) -> r, then f x is going to generalize a when typechecking x;
and of course, when instructed by an explicit annotation _ :: forall a. t a.

Inferred generic function typechecks as a return type but not an argument type

2 Answers