Zero or Logic class constraint causes ambiguous inferred type

[auricratio]

Here's a bit of code I wrote:

// zeros entries above main diagonal, doubles entries below and leaves main alone

doubleOver : {m, n, a} (fin a) => [m][n][a] -> [m][n][a]
doubleOver xss = [[f x | f <- fs | x <- xs] | fs <- fss | xs <- xss]
 where
  t0 x = 0
  t1 x = x
  t2 x = x << 1
  fs0 = [t1] # [t0 | _ <- zero]
  fss = [fs0] # [[t2] # fs | fs <- fss]

that works fine for me with Cryptol version 2.5.0 (901a1d1), but chokes for @weaversa who has a more recent version.

[brianhuffman]

With the latest version (173ca87 from Nov. 28) I get the error message, "The inferred type for doubleOver is ambiguous."

The error can be avoided by modifying the definition of fs0 from

fs0 = [t1] # [t0 | _ <- zero]

to one of the following:

fs0 = [t1] # [t0 | () <- zero]
fs0 = [t1] # [t0 | _ <- undefined]

The problem is that in _ <- zero, the type of the underscore is some unspecified type t that does not appear in the type signature, and must satisfy the class constraint Zero t. I would expect that Cryptol should specialize it to e.g. () to resolve the ambiguity, but that doesn't seem to be working.

In the first workaround, we can use () as a pattern to force type t to be (). In the second workaround, we avoid the Zero class constraint, which seems to make the specialization work.

[brianhuffman]

I'm bisecting right now to find where things go wrong. Release version 2.5.0 didn't have a Zero class yet, so I'm guessing its introduction is when the problem started.

EDIT: Bisection shows the first bad revision is d1305b2 from Sept 15, "Add 'Logic' typeclass with operations complement, &&, ||, ^, zero."

[brianhuffman]

Here's a simpler test case:

Cryptol> :t (\_ -> True) zero

[error] at <interactive>:1:1--1:18:
  The inferred type for <expr>::(expression) is ambiguous.

[yav]

I improved the ambiguity reporting in Cryptol, so now at least you can seen what's going on:

The inferred type for doubleOver is ambiguous.
Arising from:
   * a value bound by a generator in a comprehension at ./test.cry:7:16--7:33

The inferred type for <expr>::(expression) is ambiguous.
Arising from:
  * 1st type parameter
    of expression zero
    at <interactive>:1:14--1:18 at <interactive>:1:14--1:18

[yav]

A couple of related issues:

• Brian and I discussed this, and it seems like it should be safe to actually default for classes Zero, Arith and Logic, which would avoid this problem.

• Separately, it might be nice to add a replicate function to the Cryptol prelude, as this is essentially what the doubleOver example uses:

   replicate : {n,a} a -> [n] a
   replicate a = [ a | () <- zero ]
  

[brianhuffman]

NB: The Cryptol::Extras module already has repeat : {n, a} a -> [n]a.

[yav]

We don't do the ambiguity check for now, as it is a bit hard to figure out what's ambiguous. So for now,
we sometimes infer unusable types like this:

:t (\_ -> True) zero
(\_ -> True) zero : {a} (Zero a) => Bit

In the future, we may want to implement a more generic system to test for ambiguity---perhaps akin to what GHC does. It goes something like this: if f is declaration, and we compute type s for it, then we type check a new temporarily declaration of the form: newF : s; newF = f. If that succeeds, then we can accept the declaration, otherwise we reject the declaration is ambiguous.

[brianhuffman]

We might like to do defaulting for the Zero or Logic classes only at the REPL, but not for ambiguous type variables within an expression.

[robdockins]

Just checking in, current behavior is still as described by #491 (comment), which is that we will infer a polymorphic type that cannot (!) be instantiated.

[robdockins]

With the merge of #952, we now get:

Cryptol> :t (\_ -> True) zero
(\_ -> True) zero : {a} (Zero a) => Bit
Cryptol> (\_ -> True) zero
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'a' of 'Cryptol::zero'
True

So, at least at the REPL, we get some additional defaulting for these kinds of ambiguous types.

The original example still will not load.

Loading module Cryptol
Loading module Main
[error] at double.cry:7:27--7:31:
  Failed to infer the following types:
    • ?__p0`796, the type of '__p0' at double.cry:7:22--7:23
  subject to the following constraints:
    • Zero ?__p0`796
        arising from
        use of expression Cryptol::zero
        at double.cry:7:27--7:31

[robdockins]

I think we are unlikely to find a way to have the typechecker accept the original program without user annotations of some sort. I recommend using the repeat function, which is now in the prelude.