Skip to content
Snippets Groups Projects

Delicate solve order

    • Closed Issue created by Simon Peyton Jones @simonpj

    Should we successfully infer a type for f:

    f x = [h x, [x]]

    assuming h :: forall b. F b -> b?

    Assuming (x::alpha) and we instantiate h at beta, we get the constraints

     (1)  beta ~ [alpha]		from the list [h x, [x]]
 (2)  alpha ~ F beta		from the call of h

    Now if we happen to unify the constraint (1) first, beta := [alpha], then we successfully infer

    f :: forall a. (a ~ F [a]) => a -> [[a]]

    But if we unify the constraint (2) first, alpha := F beta, we get

    f :: forall b.  (b ~ [F b]) => F b -> [[F b]]

    which looks ambiguous. It isn't ambiguous, in fact, but the solver has to work hard to prove it. It actually succeeds here, but in the more complicated example in indexed-types/should_compile/IndTypesPerfMerge, it didn't. There the function merge has (a slightly more complicated form of) this delicately-balanced situation.

    But see Note [Orientation of equalities with fmvs] in TcFlatten for why we don't defer solving (2).

    Edited
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items 0

    • No child items are currently assigned. Use child items to break down this issue into smaller parts.

    Activity

    Please register or sign in to reply