Last time we concluded that typeclasses are being parsed, but they are not visible during the name resolution phase.
I won’t go over the complete timeline of my line of thought. I should have written it down but I was kind of busy with a few things and I couldn’t find the time to do it.
I made a few experiments using the final version built with GHC 8.10.2 to compare the pipeline and phases against the latest version. This was an adventure on its own, given that recent versions of Z3 are incompatible with LH in GHC 8. I had to engineer a few things to make it work, but I did it.
After all that, I got the pieces to take a stab at developing a solution:
- Typeclasses and their methods are available in the
BareSpecParsed. - To resolve logic names, the search proceeds in the following order: first looks into a local list of symbols, then looks in the
envof typeInScopeNonReflectedEnv, and it finishes its search by looking for data constructors in the scope. - The function that builds the environments to look into is
makeLogicEnvs.
One thing I noticed in my prior scouting is that typeclasses methods are stored in the sigs field of bare specs. Therefore, that’s where I was trying to retrieve them from.
Turns out it’s not as easy to identify which definitions correspond to methods and which ones come from plain functions.
After a few attempts, I noticed it might be easier to simply use the existing code to reflect the names in the signatures. The best thing, it’s just a one line change.
[ [ reflectLHName thisModule (val n)
| n <- concat
[ map fst (asmReflectSigs spec)
, HS.toList (reflects spec)
, HS.toList (opaqueReflects spec)
, HS.toList (inlines spec)
, HS.toList (hmeas spec)
+ , if allowTC then map fst (sigs spec) else []
]
]I had to add an allowTC parameter to the function and pass the result from (typeclass cfg).
Running the test, I get this error:
typeclasses/pos/Basic.hs:11:1: error:
Bad Data Specification
GHC and Liquid specifications have different numbers of fields for `Basic.C:VEq`
|
11 | class Eq a => VEq a where
| ^^^^^^^^^^^^^^^^^^^^^^^^^...It is a different message than before, so I am happy that I have some progress. This is actually the error that the first version of LH on GHC 9 (before the introduction of the LHNameResolution phase) used to throw. So, now I can focus on actually porting the functionality from GHC 8 to GHC 9.