Add scaffolfing for backtick imports

src/Cryptol/ModuleSystem/Base.hs

@@ -468,6 +468,7 @@ findDeps' m =
                   DefaultInstArg a -> loadInstArg a
                   DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds)
                   NamedInstArgs args -> mconcat (map loadNamedInstArg args)
+                  BacktickInstnace -> mempty
       in fds <> ads
     InterfaceModule s -> mconcat (map loadImpD (sigImports s))
   where

src/Cryptol/ModuleSystem/Renamer.hs

@@ -292,6 +292,7 @@ checkFunctorArgs args =
       panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"]
     DefaultInstArg l -> checkArg l
     NamedInstArgs as -> mapM_ checkNamedArg as
+    BacktickInstnace -> pure ()
   where
   checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l
 
@@ -480,6 +481,7 @@ renameTopDecls' ds =
                   DefaultInstArg arg -> depsOfArg arg
                   NamedInstArgs args -> concatMap depsOfNamedArg args
                   DefaultInstAnonArg {} -> []
+                  BacktickInstnace -> []
 
                where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a
                      depsOfArg a = case thing a of
@@ -793,6 +795,7 @@ instance Rename ModuleInstanceArgs where
       DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a
       NamedInstArgs xs -> NamedInstArgs  <$> traverse rename xs
       DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"]
+      BacktickInstnace -> pure BacktickInstnace
 
 instance Rename ModuleInstanceNamedArg where
   rename (ModuleInstanceNamedArg x m) =

src/Cryptol/Parser/AST.hs

@@ -281,6 +281,10 @@ data ModuleInstanceArgs name =
     -- (parser only)
 
   | NamedInstArgs  [ModuleInstanceNamedArg name]
+
+  | BacktickInstnace
+    -- ^ The module instance is computed by adding the functor arguments
+    -- as explicit parameters to all declarations
     deriving (Show, Generic, NFData)
 
 -- | A named argument in a functor instantiation
@@ -863,6 +867,7 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where
       DefaultInstArg x -> braces (pp (thing x))
       DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds))
       NamedInstArgs xs -> braces (commaSep (map pp xs))
+      BacktickInstnace -> "{}"
 
 instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where
   ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y)
@@ -1358,6 +1363,7 @@ instance NoPos (ModuleInstanceArgs name) where
       DefaultInstArg a      -> DefaultInstArg (noPos a)
       DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds)
       NamedInstArgs xs      -> NamedInstArgs (noPos xs)
+      BacktickInstnace      -> BacktickInstnace
 
 instance NoPos (ModuleInstanceNamedArg name) where
   noPos (ModuleInstanceNamedArg x y) =