Apalache rewritter error on poly types

[bugarela]

After solving #1393, I'm hitting another problem with the option.qnt (full) example:

error: <unknown>: rewriter error: Unexpected type a when generating a default value

https://github.com/informalsystems/apalache/blob/dd1fef9323863b49e623337fe4cba167c63f2c8d/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/DefaultValueFactory.scala#L113

[bugarela]

@shonfeder I realized I was using a reduced version of the spec for testing last Friday. We did manage to fix that problem, but once I reverted my changes to the spec, this new error appeared.

The version I was using to test it was:

module option {
  // A demonstration of sum types, specifying an option type.

  // A polymorphic option type
  type Option[a] =
    | Some(a)
    | None

  // `o.optionMap(f)` is `Some(f(v))` if `o = Some(v)` or `None` of `o = None`
  def optionMap(o, f) =
    match o {
    | Some(x) => Some(f(x))
    | None    => None
    }

  action init = true
  action step = true
 }

Going back to the full spec results in this issue's error. But I just found out something else. If we re-add the type annotation to the optionMap operator, we actually get a different version of the annotation generality error:

'unknown location,optionMap's type annotation ((None({  }) | Some(a), ((a) => b)) => None({  }) | Some(b)) is too general, inferred: ((None({  }) | Some(a), ((a) => a)) => None({  }) | Some(a))'

I'll continue digging

[shonfeder]

Oh, bummer! Possibly we have a similar issue but with the way annotations are converted?

I wonder if the

error: <unknown>: rewriter error: Unexpected type a when generating a default value

Is arising because the a free variable on the body of an expression is now now being unified away?

[bugarela]

I have two fixes locally:

1. Giving fresh names to type variables, because apalache doesn't take care of what is quantified.
2. Fixing quint type inference so it doesn't over-quantify some values

With this two, I could revert my changes on the previous Apalache PR and get the error that originated this issue

error: <unknown>: rewriter error: Unexpected type a when generating a default value

I'll take a deeper look at this error tomorrow, and then organize everything for one (or more) PR(s).

[shonfeder]

You may want to Try running on the Apalache commit before we changed where the return types where coming from too. It's possible that was is it a symptom of the same problem, and that our "fix" is responsible for this subsequent error.

[bugarela]

I've done that! That's what I meant by

With this two, I could revert my changes on the previous Apalache PR and get the error that originated this issue

(which is poorly written as I realize now. Sorry)

So I think we won't get an easy win here :/

[bugarela]

So far, for this issue, I have:

1. Fixed a type quantification problem in Quint side, which led to too general types that Apalache complained about
2. Fixed an integration problem where Apalache was not considering type variables quantified by Quint, and rather treating them as free type variables. This required a serialization fix in Quint and some logic in Apalache.

These 2 efforts result in no more errors like

'unknown location,optionMap's type annotation ((None({  }) | Some(a), ((a) => b)) => None({  }) | Some(b)) is too general, inferred: ((None({  }) | Some(a), ((a) => a)) => None({  }) | Some(a))'

Also, this ended up somehow addressing some of the rewriter problem, because the error which used to be:

error: <unknown>: rewriter error: Unexpected type a when generating a default value

After (2) is now

error: <unknown>: rewriter error: Unexpected type b when generating a default value

(changed from a to b, which means it goes through a bit further in the spec before breaking).

About this error, it is related to Apalache caches and I have no idea what is causing it.

The one thing I could find that might be a feasible fix is that, on Option.tla, our original option type implementation in TLA+, we use signatures like @type: a => $option; and @type: () => $option; for the constructor, and that works with Apalache. I thought, if changed the output produced by quint read from Apalache to, instead of inlining all occurrences of the type alias, actually keep the type alias until some level, we could achieve something similar to the current Option.tla definitions and that should work with Apalache. However, since I don't really understand the problem, I don't feel confident about putting efforts into making that change right now. I'll rather wait too see how frequent this problem appears. So far, we have only seen it in the option.qnt spec.