Record construction unsupported

[sweirich]

See examples/tests/RecordConstruction.hs

[nomeata]

Some notes while I work in on…

It’s case

convertExpr (RecordCon (L _ hsCon) PlaceHolder conExpr HsRecFields{..}) = do

in Expr.hs … ah, but the problem is that in DataType, we store an unqualified name for the field name in constructorFields. Fixing that fixes the test case, but let’s see what else breaks…

[nomeata]

Ok, this patch

diff --git a/src/lib/HsToCoq/ConvertHaskell/Declarations/DataType.hs b/src/lib/HsToCoq/ConvertHaskell/Declarations/DataType.hs
index b8a72c7..6915067 100644
--- a/src/lib/HsToCoq/ConvertHaskell/Declarations/DataType.hs
+++ b/src/lib/HsToCoq/ConvertHaskell/Declarations/DataType.hs
@@ -66,8 +66,10 @@ convertConDecl curType extraArgs (ConDeclH98 lname mlqvs mlcxt details _doc) = d

   fieldInfo <- case details of
     RecCon (L _ fields) ->
-      fmap (RecordFields . map Bare) . traverse freeVar
-        $ concatMap (map (unLoc . rdrNameFieldOcc . unLoc) . cd_fld_names . unLoc) fields
+        fmap RecordFields $
+        traverse (var ExprNS) $
+        map (selectorFieldOcc . unLoc) $
+        concatMap (cd_fld_names . unLoc) fields
     _ ->
       pure . NonRecordFields $ length args
   constructorFields . at con ?= fieldInfo

will store qualified names in constructorField, which fixes this issue. But it breaks examples/intervals. To unbreak this, the code in

convertExpr (RecordUpd recVal fields PlaceHolder PlaceHolder PlaceHolder PlaceHolder) = do
…

needs to be brought into the post-renamer era (there is still stuff mucking with OccNames instead of GHC.Name); once that uses GHC.Name and var consistently, this problem should be fixed. But there is quite a bit of non-trivial code that I do not understand there, including generation of HsSyn terms, and I would be grateful if @antalsz could pick this up

(I did not push the above fix to not introduce a regression, so apply that or something equivalently when you fix this bug.)

@antalsz, note that Stephanie’s testcase looks succeeding already, but there is a missingValue that goes away with this patch.