Haskell error: Could not deduce (Random a0)

user_4078958 0
Viewed 89

I'm trying to make another Random instance but get stuck on a type error. I reduced it to the following ghci session:

GHCi, version 8.6.5:
λ> import System.Random
λ> :t random
random :: (Random a, RandomGen g) => g -> (a, g)
λ> :t \g -> random g
\g -> random g :: (Random a, RandomGen g) => g -> (a, g)
λ> :t \g -> let xh = random g in xh
\g -> let xh = random g in xh
  :: (Random a, RandomGen g) => g -> (a, g)
λ> :t \g -> let (x, h) = random g in (x, h)

<interactive>:1:11: error:
    • Could not deduce (Random a0)
      from the context: (Random a, RandomGen b)
        bound by the inferred type of
                   it :: (Random a, RandomGen b) => b -> (a, b)
        at <interactive>:1:1
      The type variable ‘a0’ is ambiguous
    • When checking that the inferred type
        h :: forall a. Random a => b
      is as general as its inferred signature
        h :: b
      In the expression: let (x, h) = random g in (x, h)
      In the expression: \ g -> let (x, h) = ... in (x, h)

Why does it fail in the last version?

typeerror haskell
1 Answers

It's a cute problem. You're probably imagining that this gets translated into explicit-dictionary-passing-style something like this:

-- original
foo = \g -> let (x, h) = random g in (x, h)

-- assumed but incorrect explicit version
foo = /\a. /\b. \\(da :: Random a) => \\(db :: RandomGen b) =>
    \(g :: b) -> let tmp = random @a @b ,da ,db g
                     x = case tmp of (x, h) -> x
                     h = case tmp of (x, h) -> h
                 in (x, h)

Here I'm using some custom new pieces of syntax:

  • /\ty. tm is explicit type abstraction; it takes a type, names it ty, and proceeds as the term tm does
  • tm @ty is explicit type application; it takes a polymorphic term tm and supplies ty as the first type argument
  • \\(dict :: c) => tm is explicit typeclass abstraction; it takes a typeclass dictionary that is evidence of the constraint c, names it dict, and proceeds as the term tm does
  • tm ,dict is explicit typeclass application; it takes a term that assumes some typeclass instance, and supplies the dictionary dict as evidence of that instance

If this were how the thing was compiled, then there'd be no ambiguity, and \g -> let (x, h) = random g in (x, h) would have just the same type as all the previous terms. But that is not how pattern bindings are actually compiled, because that makes the types of x and h more restrictive than they need to be. Instead, it's compiled this way:

-- actual explicit version
foo = /\a. /\b. /\c. \\(da :: Random a) => \\(db :: Random b) => \\(dc :: RandomGen c) =>
    \(g :: b) -> let x = /\d. \\(dd :: Random d) =>
                         case random @d @c ,dd ,dc g of (x, h) -> x
                     h = /\d. \\(dd :: Random d) =>
                         case random @d @c ,dd ,dc g of (x, h) -> h
                 in (x @a ,da , h @b ,db)

This one is more polymorphic, because the type used to choose a Random instance while computing x is not tied to the type used to choose a Random instance while computing h. In this case it isn't what you want; but it is possible to dream up other situations where this is just what you want, and tying the two types together is quite inconvenient for expressing the computation you want.

But, because of the extra flexibility this translation allows, we find ourself in a bit of a bind here: it's not so obvious how the caller of this thing could influence which type was chosen for b (hence which dictionary to use for db), since b doesn't appear anywhere in the type of the overall thing! So the compiler gives you a type ambiguity error. As an intuitive explanation: we know which Random instance to use for computing x because the caller has to pick a type for the first part of the tuple; but we don't know which instance to use for computing h because choosing a type for h doesn't nail down what type to use for the discarded x half of the computation used to define h.

You may ask the compiler to choose the first translation by enabling the MonoLocalBinds extension. You can read more about it here. It sometimes prevents let bindings from becoming polymorphic in the way described above, which means that type inference will have more clues but that some otherwise-acceptable programs will no longer typecheck.

user_7916040
Related