Unresolved numeric contexts that should be resolvable

[krame505]

The background for this is that my GenCRepr library uses a variable-width, byte-packed serialization format. The current implementation generates very inefficient hardware for sequences of variable-width items, such as like Vector 100 (Maybe Bool) - the number of cases ends up being exponential in the size of the vector. I have been trying to make this more efficient by instead tracking the running size of the message and generating multiplexers to read/write the appropriate offset in the message being packed/unpacked. The code for this is currently at https://github.com/krame505/bsc-contrib/tree/genc-encode-vector.

However, I have been seeing some errors about unresolved contexts that I don't understand:

Error: "Test.bs", line 9, column 0: (T0032)
  This expression requires the following context which could not be resolved:
    GenCRepr.GenCRepr Test.Enum a__
  The context was implied by expressions at the following positions:
    "Test.bs", line 10, column 10
  An instance for this context exists, but it depends on the following
  contexts for which there are no instances:
    Prelude.Max 1 1 1,
    Prelude.Add 1 b__ 1

Both of these contexts seemingly should be trivially satisfied? This is either a bug in context reduction, or else a symptom of another error in my code that isn't being reported properly. I added the file that caused this error at https://github.com/krame505/bsc-contrib/blob/genc-encode-vector/Libraries/GenC/Test.bs.

[quark17]

Is the i2 in the base type here a mistake, should it be i (which is either i1 or i2 depending on which of n1 or n2 was the max n)?

instance (UnpackUnionBody tagBytes a i1 n1 m, UnpackUnionBody tagBytes b i2 n2 m,
          Max n1 n2 n,
          Add tagBytes k m, Add n1 k1 m, Add n2 k2 m) =>
         UnpackUnionBody tagBytes (Either a b) i2 n m where

Anyway, BSC has determined that GenCRepr Enum a can't be satisfied, and it used to be that BSC would just say that, but now there's code which attempts to reconstruct why. That code is in ContextErrors.hs and it just takes the unsatisfied context and tried to reduce it and see where it gets to, and report that. There's also code that knows about specific typeclasses (PrimBitExtend, PrimSelectable, PrimWriteable, PrimIndex, IsModule, etc) and for those BSC will attempt to report a message in text that is more familiar to the user. In this case, though, none of the primitive classes are involved, so it's just printing out the contexts. (Specifically, it's handleContextReduction that is called, passing in GenCRepr, and that does some attempted reduction and then passes it to handleContextReduction' which has arms for each of the primitive typeclasses, but that falls through to the end, which calls defaultContextReductionErr to construct the default message.)

My guess is that Add 1 b__ 1 can't resolve because b__ is a dependent variable. Yes, it could normally be satisfied by assing b__ to 0, but that's only possible for free variables, and if b__ is bound then we can't assign, we just need to be told. Some possibly in one of your instances, you need to write 0 in place of a variable name. (Or else, your provisos have a bug in them that leads to b__ being 0 and you need to rewrite the provisos so that they don't imply that.)

BSC could be doing a better job of showing you the trace of the instances that it went through, to get to that point, and that could help identify what b__ refers to in the source. You could try turning on trace flags, to see if BSC can dump some into. (ContextErrors has a function findReducedPreds which it uses, and that calls reducePredsAggressive in TCMisc, which calls satMany, which has traces that can be turned on with -trace-type.)

I would guess that Max 1 1 1 is showing up because handleContextReduction is just showing you all of the provisos that are needed for the final instance, and it hasn't filtered out the ones that can be satisfied. Maybe?

FYI, I did find some code that surprised me. It may not the be the cause of your problem, because fixing it doesn't fix the problem. But I notice that you have some classes defined like this:

class UnpackBytes a n m | a m -> n where
  unpackBytesM :: (Add n k m) => ByteDecoder m a

Here, the proviso has variables n and k that don't appear in the base type (ByteDecoder m a)! But I guess this works because n is determined by m and a that are in the base type? Anyway, I rewrote it to remove Add n k m from the function. Possibly you put it there because BSC currently doesn't allow you to make it a superclass:

class (Add n k m) => UnpackBytes a n m | a m -> n where

I was able to workaround that using Max n m m (assuming you need a superclass at all) and then putting Add n k m in the places that use the class (which is usually in the instances) -- and the only reason that Add n k m needs to be specified explicitly (if Max n m m is already stated) is because of a limitation in BSC's solver, that hopefully one day we fix (and then the explicit proviso won't be needed). (The limitation is that Max n m m can be resolved knowing Add n k m, but the other way around can't currently be done because resolving Add n k m requires learning a substitution for k, and BSC's use of the SMT solver doesn't yet allow learning of such assignments.) But anyway, making that change (in multiple classes) just gets back to the original issue, so it's probably not the source of your problem.

[quark17]

I notice that in the instance for GenCUnionBody of Either, you have a proviso that declares tagBits, but then it is unused, and in the member functions, you only use tagBytes -- could that be part of the problem? Should you be using Bit tagBits in some of the places where you have Bit tagBytes?

[quark17]

The trace seems to suggest that BSC ends up with this:

Prelude.Max _tctyvar2725 1 1,
Prelude.Add _tctyvar2725 _tctyvar2726 1

and it deduces that _tctyvar2725 is 1, but that's not enough to reduce the whole thing.

And I think that earlier they were this (but _tctyvar1008 was determined to be 1):

Prelude.Add _tctyvar2725 _tctyvar2726 _tctyvar1008,
Prelude.Max _tctyvar2725 1 _tctyvar1008

And specifically, _tctyvar1008 is the UnpackBytes needed for the representation of Enum, because we have these:

Generic Enum _tctyvar2230
UnpackBytes' _tctyvar2230 _tctyvar1008 _tctyvar1008

I also see that earlier BSC encounters this:

UnpackUnionBody
  1
  (Prelude.Either (Prelude.Meta (Prelude.MetaConsAnon "E1" 0 0) ())
                  (Prelude.Meta (Prelude.MetaConsAnon "E2" 1 0) ()))
  _tctyvar2733
  _tctyvar2725
  _tctyvar1008

which suggests that it has figured out that tagBytes is 1 and we can see that _tctyvar2725 is n and _tctyvar1008 is m. (And _tctyvar2733 is i, which it later figures out is 1.) So our unsolved provisos would be roughly something like this:

Prelude.Max n 1 m,
Prelude.Add n _tctyvar2726 m

And best I can tell _tctyvar2726 comes from the k1 when resolving this instance:

instance (UnpackUnionBody tagBytes a i1 n1 m, UnpackUnionBody tagBytes b i2 n2 m,
          Max n1 n2 n,
          Add tagBytes k m, Add n1 k1 m, Add n2 k2 m) =>
         UnpackUnionBody tagBytes (Either a b) i2 n m where

But I don't know why it wouldn't be able to conclude that k2 is zero.

[quark17]

Ah, nevermind. It does look like a bug in BSC.

BSC can be made to compile the example by changing line 427 in TCMisc from this:

satMany dvs es (needed ++ rs_accum) (bs'++bs) (s' @@ s) ps

to this:

satMany dvs es ((apSub s' needed) ++ rs_accum) (bs'++bs) (s' @@ s) ps

This is in a case-arm where BSC's proviso satisfier has determined that a proviso can be resolved, but it introduces new provisos that need to be resolved, as well as a substitution of what was learned in the process. What was happening was that the needed provisos had types that could be substituted with more concrete information. Specifically, I noticed that Max 1 1 1 or Add 1 b__ 1 couldn't be resolved because they didn't have 1s in them, they still had variable names -- but there were learned substitutions for those variables to 1. Anyway, the above change applies the substitution to the needed provisos, to put them in a concrete form that can be easily resolved.

I don't know if this is necessarily the best change, though. Maybe the place that produced the needed provisos should have applied the substitution first? (I assume that it's not the responsibility of a later place to apply the substitution; because we want to avoid unnecessary re-application of the substititon, I suspect.) It may be that the substitution needs to be applied to the bindings -- and that the variables only show up in the later provisos because we've left them in the bindings. Or maybe we need both?

Anyway, I discovered the issue by looking in the trace from -trace-type. I could see output beginning with sat=, which dumps the triple of needed provisos, new bindings, and new substitutions. I saw that there was output which showed the Max/Add as needed, but their first variable was in the substitution being replaced with 1. However, if look further up in the output, I see that there is first a line which has the variable in a binding, before it ever appears in a proviso. So maybe applying the substitution to the bindings would be enough? Or maybe the bindings can be substituted at the point where they are created? (And which is the most efficient? Is there less application on the needed provisos than on the bindings?)

[quark17]

I observe that applying the substitution to the bindings (even to the existing ones) doesn't help BSC get past the error. So applying to the needed provisos may be the right thing.

[krame505]

Thank you for taking time to look into this! Yes, the above change you mentioned in TCMisc does seem to solve the error for now.