Comments (6)
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.
from bsc.
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
?
from bsc.
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.
from bsc.
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?)
from bsc.
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.
from bsc.
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.
from bsc.
Related Issues (20)
- `-dparsed` output produces invalid register updates with BSV HOT 2
- `-dparsed` produces invalid BSV module function that takes another module as an argument HOT 2
- Missing `Ord Bool` instance HOT 7
- Static check of file descriptor argument to tasks like $fgetc HOT 3
- Testsuite reports an error getting BSC version HOT 2
- Internal Compiler Error when quoting a character value. HOT 4
- Bluesim's symbol-probing interface has wrong values for FIFO
- Verilog import fails in macro substitution HOT 2
- Unexpected syntax error HOT 1
- expandPorts.tcl has hardcoded paths which do not exist. HOT 1
- Unexpected behavior in Stmt sequence when using par HOT 2
- Bluesim divide-by-zero behavior is inconsistent on arm64 HOT 2
- Type synonyms with phantom parameters can lead to strange behaviors (E.g., compiler hang) HOT 4
- doc example for mkUniqueWrapper2 HOT 7
- -remove-unused-modules flag doesn't work with mkProbe module provided in std library HOT 2
- Failures with compilation on raspberry-pi 5 HOT 4
- GCC 14 emits extra warnings HOT 1
- Github's macos-11 runner is going away HOT 1
- [Bluesim] Simulation executable fails with `undefined symbol: _Z21vcd_write_scope_startP9tSimStatePKc` HOT 9
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bsc.