Upgrade hs-to-coq to GHC 8.6, 8.8, 8.10

- Use CPP to adapt to the "Trees That Grow" update to GHC's ASTs.
- CPP doesn't like Haskell multiline strings because of the trailing
  backslash, so they were made single-line.
- CPP also gets confused by quotes, so for instance convertType' had to be
  renamed to convertType_ to allow macros to expand.

Warn about unsupported top-level bindings

- Skip pattern synonyms rather than error

hs-to-coq.cabal

@@ -13,12 +13,20 @@ copyright:           Copyright © 2016 Antal Spector-Zabusky, University of Penn
 category:            Language
 build-type:          Simple
 cabal-version:       >=1.10
-extra-source-files:  src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y
+extra-source-files:
+  src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y
+  src/include/*.h
+tested-with: GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4 GHC == 8.10.1
 
 source-repository head
   type:     git
   location: https://github.com/antalsz/hs-to-coq
 
+flag legacy-warnings
+  description: Reenable -Wincomplete-patterns for newer versions of GHC
+  manual: True
+  default: False
+
 library
   exposed-modules:     HsToCoq.Util.GHC
                      , HsToCoq.Util.GHC.Module
@@ -106,30 +114,30 @@ library
                      , TemplateHaskell
                      , CPP
 
-  build-depends:       base                 ==4.11.*
-                     , template-haskell     ==2.13.*
-                     , ghc                  ==8.4.*
-                     , ghc-boot             ==8.4.*
-                     , ghc-paths            ==0.1.*
-                     , bifunctors           ==5.*
-                     , semigroups           ==0.18.*
-                     , transformers         ==0.5.*
-                     , mtl                  ==2.2.*
-                     , array                ==0.5.*
-                     , lens                 ==4.16.*
-                     , pipes                ==4.3.*
-                     , containers           ==0.5.*
-                     , contravariant        >=1.3 && <1.6
-                     , validation           ==1.*
-                     , syb                  ==0.7.*
-                     , text                 ==1.2.*
-                     , directory            ==1.3.*
-                     , filepath             ==1.4.*
-                     , wl-pprint-text       ==1.2.*
-                     , parsec               ==3.1.*
-                     , indents              ==0.5.*
-                     , optparse-applicative ==0.14.*
-                     , yaml                 ==0.8.*
+  build-depends:       base                 >=4.11 && < 4.15
+                     , template-haskell     >=2.13
+                     , ghc                  >=8.4
+                     , ghc-boot
+                     , ghc-paths
+                     , bifunctors
+                     , semigroups
+                     , transformers
+                     , mtl
+                     , array
+                     , lens
+                     , pipes
+                     , containers
+                     , contravariant
+                     , validation
+                     , syb
+                     , text
+                     , directory
+                     , filepath
+                     , wl-pprint-text
+                     , parsec
+                     , indents
+                     , optparse-applicative
+                     , yaml
 
   -- These are actually not used directly by hs-to-coq, but work around a
   -- bug(?) in GHC-8.4 that no longer loads other packages if there is a GHC
@@ -139,14 +147,16 @@ library
     test-framework-quickcheck2 >= 0.2.9,
     test-framework-hunit
 
-
   hs-source-dirs:      src/lib
+  include-dirs:        src/include
   default-language:    Haskell2010
   ghc-options:         -Wall -fno-warn-name-shadowing
+  if !flag(legacy-warnings) && impl(ghc >= 8.6)
+    ghc-options:       -Wno-unused-imports
 
 executable hs-to-coq
   main-is:             Main.hs
-  build-depends:       base == 4.11.*, hs-to-coq
+  build-depends:       base, hs-to-coq
   hs-source-dirs:      src/exe
   default-language:    Haskell2010
   ghc-options:         -Wall -fno-warn-name-shadowing

src/include/ghc-compat.h

@@ -0,0 +1,49 @@
+#ifndef __GHC_COMPAT__
+#define __GHC_COMPAT__
+
+#if 0
+GHC 8.6 started using extensively the "Trees That Grow" style of ASTs,
+which extends many constructors with a new "extension field".
+
+To maintain compatibility across that change, this header introduces some
+macros that either expand to the new field when it exists (GHC >= 8.6)
+or disappear when it doesn't exist (GHC < 8.6).
+
+> f (HsApp NOEXTP x y) = ...  -- before CPP
+> f (HsApp _ x y) = ...       -- after CPP, GHC >= 8.6
+> f (HsApp x y) = ...         -- after CPP, GHC 8.4
+
+- Since GHC 8.10, inactive extension fields have type 'NoExtField'
+- On GHC 8.6 and GHC 8.8, inactive extension fields have a differently named
+  type 'NoExt'
+- On GHC 8.4, some AST nodes already had "Trees That Grow"-style extension fields,
+  with the default type 'PlaceHolder', that we rename accordingly in newer versions
+  by turning it into a macro.
+
+- The macro 'NOEXT' expands to the constructor name ('NoExtField', 'NoExt'),
+  which can be used as both an expression and a pattern.
+- The macro 'NOEXTP' expands to a wildcard pattern, which can be used for
+  pattern-matching when the extension field is not inactive (not of type
+  'NoExtField' or 'NoExt').
+#endif
+
+#if __GLASGOW_HASKELL__ >= 810
+
+#define PlaceHolder NoExtField
+#define NOEXT NoExtField
+#define NOEXTP _
+
+#elif __GLASGOW_HASKELL__ >= 806
+
+#define PlaceHolder NoExt
+#define NOEXT NoExt
+#define NOEXTP _
+
+#else
+
+#define NOEXT
+#define NOEXTP
+
+#endif
+
+#endif

src/lib/HsToCoq/ConvertHaskell/Declarations/Class.hs

@@ -1,4 +1,6 @@
-{-# LANGUAGE RecordWildCards, LambdaCase, ViewPatterns, FlexibleContexts, OverloadedStrings, OverloadedLists, ScopedTypeVariables, MultiParamTypeClasses #-}
+{-# LANGUAGE CPP, RecordWildCards, LambdaCase, ViewPatterns, FlexibleContexts, OverloadedStrings, OverloadedLists, ScopedTypeVariables, MultiParamTypeClasses #-}
+
+#include "ghc-compat.h"
 
 module HsToCoq.ConvertHaskell.Declarations.Class (ClassBody(..), convertClassDecl, getImplicitBindersForClassMember, classSentences, directClassSentences, cpsClassSentences, convertAssociatedType, convertAssociatedTypeDefault) where
 
@@ -30,6 +32,9 @@ import HsToCoq.Coq.Gallina.Util
 import HsToCoq.Coq.Gallina.Rewrite
 import HsToCoq.Coq.Pretty
 import HsToCoq.Util.FVs
+#if __GLASGOW_HASKELL__ >= 806
+import HsToCoq.Util.GHC.HsTypes (noExtCon)
+#endif
 
 import HsToCoq.ConvertHaskell.TypeInfo
 import HsToCoq.ConvertHaskell.Monad
@@ -70,7 +75,7 @@ getImplicits (Forall bs t) = if length bs == length imps then imps ++ getImplici
 getImplicits _ = []
 
 -- Module-local
-convUnsupportedIn_lname :: (ConversionMonad r m, Outputable nm) => String -> String -> GenLocated l nm -> m a
+convUnsupportedIn_lname :: (ConversionMonad r m, Outputable nm) => String -> String -> Located nm -> m a
 convUnsupportedIn_lname what whatFam lname = do
   name <- T.unpack <$> ghcPpr (unLoc lname)
   convUnsupportedIn what whatFam name
@@ -82,7 +87,7 @@ convertAssociatedType classArgs FamilyDecl{..} = do
   case fdInfo of
     OpenTypeFamily     -> pure ()
     DataFamily         -> badAssociation "associated data types"           "data family"
-    ClosedTypeFamily _ -> badAssociation "associated closed type families" "closed type family "
+    ClosedTypeFamily _ -> badAssociation "associated closed type families" "closed type family"
   -- Skipping 'fdFixity'
   unless (null fdInjectivityAnn) $ badAssociation "injective associated type families" "associated type"
 
@@ -92,28 +97,58 @@ convertAssociatedType classArgs FamilyDecl{..} = do
   unless (classArgs == foldMap (toListOf binderIdents) args) $
     badAssociation "associated type families with argument lists that differ from the class's" "associated type"
   storeExplicitMethodArguments name args
-  
+
   result <- case unLoc fdResultSig of
-    NoSig                            -> pure $ Sort Type
-    KindSig   k                      -> withCurrentDefinition name $ convertLType k
-    TyVarSig (L _ (UserTyVar _))     -> pure $ Sort Type -- Maybe not a thing inside type classes?
-    TyVarSig (L _ (KindedTyVar _ k)) -> withCurrentDefinition name $ convertLType k   -- Maybe not a thing inside type classes?
+    NoSig NOEXTP                     -> pure $ Sort Type
+    KindSig NOEXTP k                 -> withCurrentDefinition name $ convertLType k
+    TyVarSig NOEXTP (L _ (UserTyVar NOEXTP _))
+      -> pure $ Sort Type -- Maybe not a thing inside type classes?
+    TyVarSig NOEXTP (L _ (KindedTyVar NOEXTP _ k))
+      -> withCurrentDefinition name $ convertLType k   -- Maybe not a thing inside type classes?
+#if __GLASGOW_HASKELL__ >= 806
+    TyVarSig _ (L _ (XTyVarBndr v)) -> noExtCon v
+    XFamilyResultSig v -> noExtCon v
+#endif
 
   pure (name, result)
 
-convertAssociatedTypeDefault :: ConversionMonad r m => [Qualid] -> TyFamDefltEqn GhcRn -> m (Qualid, Term)
-convertAssociatedTypeDefault classArgs FamEqn{..} = do
+#if __GLASGOW_HASKELL__ >= 806
+convertAssociatedType _ (XFamilyDecl v) = noExtCon v
+#endif
+
+#if __GLASGOW_HASKELL__ < 810
+type TyFamDefltDecl pass = TyFamDefltEqn pass
+type LTyFamDefltDecl pass = LTyFamDefltEqn pass
+#endif
+
+convertAssociatedTypeDefault
+  :: ConversionMonad r m
+  => [Qualid]
+  -> TyFamDefltDecl GhcRn
+  -> m (Qualid, Term)
+convertAssociatedTypeDefault classArgs
+#if __GLASGOW_HASKELL__ >= 810
+    (TyFamInstDecl { tfid_eqn = HsIB { hsib_body = FamEqn{..} } })
+      | let params = fromMaybe [] feqn_bndrs = do
+#else
+    FamEqn{..} | let params = hsq_explicit feqn_pats = do
+#endif
   n <- var TypeNS (unLoc feqn_tycon)
-  args <- withCurrentDefinition n (convertLHsTyVarBndrs Coq.Explicit $ hsq_explicit feqn_pats)
+  args <- withCurrentDefinition n (convertLHsTyVarBndrs Coq.Explicit params)
   unless (classArgs == foldMap (toListOf binderIdents) args) $
     convUnsupportedIn_lname "associated type family defaults with argument lists that differ from the class's"
                             "associated type equation"
                             feqn_tycon
   ty <- withCurrentDefinition n $ convertLType feqn_rhs
   pure (n, ty)
-
   -- Skipping feqn_fixity
-
+
+#if __GLASGOW_HASKELL__ >= 810
+convertAssociatedTypeDefault _ (TyFamInstDecl (HsIB { hsib_body = XFamEqn v })) = noExtCon v
+#elif __GLASGOW_HASKELL__ >= 806
+convertAssociatedTypeDefault _ (XFamEqn v) = noExtCon v
+#endif
+
 convertClassDecl :: ConversionMonad r m
                  => LHsContext GhcRn                      -- ^@tcdCtxt@    Context
                  -> Located GHC.Name                      -- ^@tcdLName@   name of the class
@@ -122,7 +157,7 @@ convertClassDecl :: ConversionMonad r m
                  -> [LSig GhcRn]                          -- ^@tcdSigs@    method signatures
                  -> LHsBinds GhcRn                        -- ^@tcdMeths@   default methods
                  -> [LFamilyDecl GhcRn]                   -- ^@tcdATs@     associated types
-                 -> [LTyFamDefltEqn GhcRn]                -- ^@tcdATDefs@  associated types defaults
+                 -> [LTyFamDefltDecl GhcRn]               -- ^@tcdATDefs@  associated types defaults
                  -> m ClassBody
 convertClassDecl (L _ hsCtx) (L _ hsName) ltvs fds lsigs defaults types typeDefaults = do
   name <- var TypeNS hsName

src/lib/HsToCoq/ConvertHaskell/Declarations/DataType.hs

@@ -1,7 +1,11 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TupleSections, RecordWildCards, LambdaCase,
              OverloadedStrings,
              FlexibleContexts #-}
 
+#include "ghc-compat.h"
+
 module HsToCoq.ConvertHaskell.Declarations.DataType (
   convertDataDecl,
   ) where
@@ -15,6 +19,7 @@ import Data.Semigroup (Semigroup(..))
 import Data.Foldable
 import Data.Traversable
 import Data.Maybe
+import HsToCoq.Util.Monad (failEither)
 import HsToCoq.Util.Traversable
 
 import qualified Data.Set        as S
@@ -27,6 +32,11 @@ import Control.Monad.Trans.Maybe
 import GHC hiding (Name)
 import qualified GHC
 
+import HsToCoq.Util.GHC.HsTypes (selectorFieldOcc_)
+#if __GLASGOW_HASKELL__ >= 806
+import HsToCoq.Util.GHC.HsTypes (noExtCon)
+#endif
+
 import HsToCoq.Coq.Gallina as Coq
 import HsToCoq.Coq.Gallina.Util
 
@@ -64,21 +74,29 @@ conNameOrSkip name = do
 
 convertConDecl :: ConversionMonad r m
                => Term -> [Binder] -> ConDecl GhcRn -> m [Constructor]
-convertConDecl curType extraArgs (ConDeclH98 lname mlqvs mlcxt details _doc) = fmap fold . runMaybeT $ do
+#if __GLASGOW_HASKELL__ >= 806
+convertConDecl _ _ (XConDecl v) = noExtCon v
+convertConDecl curType extraArgs (ConDeclH98
+    { con_name = lname, con_ex_tvs = lqvs, con_mb_cxt = mlcxt, con_args = details }) =
+#else
+convertConDecl curType extraArgs (ConDeclH98 lname mlqvs mlcxt details _doc)
+ | let lqvs = maybe [] hsq_explicit mlqvs =
+#endif
+ fmap fold . runMaybeT $ do
   unless (maybe True (null . unLoc) mlcxt) $ convUnsupported' "constructor contexts"
 
   con <- conNameOrSkip $ unLoc lname
 
   -- Only the explicit tyvars are available before renaming, so they're all we
   -- need to consider
-  params <- withCurrentDefinition con $ maybe (pure []) (convertLHsTyVarBndrs Coq.Implicit . hsq_explicit) mlqvs
+  params <- withCurrentDefinition con $ convertLHsTyVarBndrs Coq.Implicit lqvs
   args   <- withCurrentDefinition con (traverse convertLType $ hsConDeclArgTys details)
 
   case details of
     RecCon (L _ fields) ->
       do
        let qualids =  traverse (var ExprNS) $
-                      map (selectorFieldOcc . unLoc) $
+                      map (selectorFieldOcc_ . unLoc) $
                       concatMap (cd_fld_names . unLoc) fields
        fieldInfo <- fmap RecordFields qualids
        storeConstructorFields con fieldInfo
@@ -91,14 +109,24 @@ convertConDecl curType extraArgs (ConDeclH98 lname mlqvs mlcxt details _doc) = f
       storeConstructorFields con fieldInfo
       pure [(con, params , Just . maybeForall extraArgs $ foldr Arrow curType args)]
 
+#if __GLASGOW_HASKELL__ >= 806
+convertConDecl curType extraArgs (ConDeclGADT
+    { con_names = lnames, con_qvars = qvars, con_mb_cxt = mcxt
+    , con_args = args, con_res_ty = res_ty }) = do
+#else
 convertConDecl curType extraArgs (ConDeclGADT lnames sigTy _doc) = do
+#endif
   fmap catMaybes . for lnames $ \(L _ hsName) -> runMaybeT $ do
     conName         <- conNameOrSkip hsName
     utvm            <- unusedTyVarModeFor conName
-    (_, curTypArgs) <- collectArgs curType
-    conTy           <- withCurrentDefinition conName 
-                       (maybeForall extraArgs <$> convertLHsSigTypeWithExcls utvm sigTy
-                         (mapMaybe termHead curTypArgs))
+    (_, curTypArgs) <- failEither (collectArgs curType)
+    conTy           <- withCurrentDefinition conName $
+#if __GLASGOW_HASKELL__ >= 806
+      let mktm = convertHsSigType_ utvm qvars mcxt args res_ty in
+#else
+      let mktm = convertLHsSigTypeWithExcls utvm sigTy in
+#endif
+      maybeForall extraArgs <$> mktm (mapMaybe termHead curTypArgs)
     storeConstructorFields conName $ NonRecordFields 0   -- This is a hack
     pure (conName, [], Just conTy)
 
@@ -150,11 +178,14 @@ rewriteDataTypeArguments dta bs = do
 convertDataDefn :: LocalConvMonad r m
                 => Term -> [Binder] -> HsDataDefn GhcRn
                 -> m (Term, [Constructor])
-convertDataDefn curType extraArgs (HsDataDefn _nd lcxt _ctype ksig cons _derivs) = do
+convertDataDefn curType extraArgs (HsDataDefn NOEXTP _nd lcxt _ctype ksig cons _derivs) = do
   unless (null $ unLoc lcxt) $ convUnsupported' "data type contexts"
   (,) <$> maybe (pure $ Sort Type) convertLType ksig
       <*> (traverse addAdditionalConstructorScope =<<
            foldTraverse (convertConDecl curType extraArgs . unLoc) cons)
+#if __GLASGOW_HASKELL__ >= 806
+convertDataDefn _ _ (XHsDataDefn v) = noExtCon v
+#endif
 
 convertDataDecl :: ConversionMonad r m
                 => Located GHC.Name -> [LHsTyVarBndr GhcRn] -> HsDataDefn GhcRn
@@ -165,10 +196,14 @@ convertDataDecl name tvs defn = do
   kinds     <- (++ repeat Nothing) . map Just . maybe [] NE.toList <$> view (edits.dataKinds.at coqName)
   let cvtName tv = Ident <$> var TypeNS (unLoc tv)
   let  go :: ConversionMonad r m => LHsTyVarBndr GhcRn -> Maybe Term -> m Binder
-       go (L _ (UserTyVar name))     (Just t) = cvtName name >>= \n -> return $ Typed Ungeneralizable Coq.Explicit (n NE.:| []) t
-       go (L _ (UserTyVar name))     Nothing  = cvtName name >>= \n -> return $ Inferred Coq.Explicit n
-       go (L _ (KindedTyVar name _)) (Just t) = cvtName name >>= \n -> return $ Typed Ungeneralizable Coq.Explicit (n NE.:| []) t
-       go (L _ (KindedTyVar name _)) Nothing  = cvtName name >>= \n -> return $ Inferred Coq.Explicit n  -- dunno if this could happen
+       go (L _ (UserTyVar NOEXTP name))     (Just t) = cvtName name >>= \n -> return $ Typed Ungeneralizable Coq.Explicit (n NE.:| []) t
+       go (L _ (UserTyVar NOEXTP name))     Nothing  = cvtName name >>= \n -> return $ Inferred Coq.Explicit n
+       go (L _ (KindedTyVar NOEXTP name _)) (Just t) = cvtName name >>= \n -> return $ Typed Ungeneralizable Coq.Explicit (n NE.:| []) t
+       go (L _ (KindedTyVar NOEXTP name _)) Nothing  = cvtName name >>= \n -> return $ Inferred Coq.Explicit n  -- dunno if this could happen
+#if __GLASGOW_HASKELL__ >= 806
+       go (L _ (XTyVarBndr v)) _ = noExtCon v
+#endif
+
   rawParams <- zipWithM go tvs kinds
 
   (params, indices) <-