A not very tested implantation of backitick imports

The actual backtick syntactic sugar still needs to be
implemented, at the moment we use

module M = F {_}

The plan is that
import `F
is syntactic sugar for
module M = F {_}
import M

src/Cryptol/Parser.y

@@ -196,6 +196,8 @@ namedModInstParam          :: { ModuleInstanceNamedArg PName }
 modInstParam               :: { Located (ModuleInstanceArg PName) }
   : impName                   { fmap ModuleArg $1 }
   | 'interface' ident         { fmap ParameterArg $2 }
+  | '_'                       { Located { thing    = AddParams
+                                        , srcRange = $1 } }
 
 vmod_body                  :: { [TopDecl PName] }
   : vtop_decls                { reverse $1 }

src/Cryptol/TypeCheck/AST.hs

@@ -19,7 +19,7 @@ module Cryptol.TypeCheck.AST
   , Name()
   , TFun(..)
   , Selector(..)
-  , Import, ImportG(..)
+  , Import, ImportG(..), ImpName(..)
   , ImportSpec(..)
   , ExportType(..)
   , ExportSpec(..), isExportedBind, isExportedType, isExported
@@ -41,7 +41,9 @@ import Cryptol.ModuleSystem.Exports(ExportSpec(..)
 import Cryptol.Parser.AST ( Selector(..),Pragma(..)
                           , Import
                           , ImportG(..), ImportSpec(..), ExportType(..)
-                          , Fixity(..))
+                          , Fixity(..)
+                          , ImpName(..)
+                          )
 import Cryptol.Utils.RecordMap
 import Cryptol.TypeCheck.FFI.FFIType
 import Cryptol.TypeCheck.PP

src/Cryptol/TypeCheck/Error.hs

@@ -155,8 +155,7 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
               | FunctorInstanceMissingArgument Ident
               | FunctorInstanceBadArgument Ident
               | FunctorInstanceMissingName Namespace Ident
-              | FunctorInstanceBadBacktickArgument Ident Ident
-                -- ^ Name of functor argument, name of bad value
+              | FunctorInstanceBadBacktick BadBacktickInstance
 
               | UnsupportedFFIKind TypeSource TParam Kind
                 -- ^ Kind is not supported for FFI
@@ -180,6 +179,14 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
                 -- implementation.
                 deriving (Show, Generic, NFData)
 
+data BadBacktickInstance =
+    BIPolymorphicArgument Ident Ident
+  | BINested [(BIWhat, Name)]
+    deriving (Show, Generic, NFData)
+
+data BIWhat = BIFunctor | BIInterface | BIPrimitive | BIForeign | BIAbstractType
+    deriving (Show, Generic, NFData)
+
 -- | When we have multiple errors on the same location, we show only the
 -- ones with the has highest rating according to this function.
 errorImportance :: Error -> Int
@@ -193,7 +200,7 @@ errorImportance err =
     MissingModParam {}                                -> 10
     FunctorInstanceBadArgument {}                     -> 10
     FunctorInstanceMissingName {}                     ->  9
-    FunctorInstanceBadBacktickArgument {}             ->  9
+    FunctorInstanceBadBacktick {}                     ->  9
 
 
     KindMismatch {}                                  -> 10
@@ -300,7 +307,7 @@ instance TVars Error where
       FunctorInstanceMissingArgument {} -> err
       FunctorInstanceBadArgument {} -> err
       FunctorInstanceMissingName {} -> err
-      FunctorInstanceBadBacktickArgument {} -> err
+      FunctorInstanceBadBacktick {} -> err
 
       UnsupportedFFIKind {}    -> err
       UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
@@ -349,7 +356,7 @@ instance FVS Error where
       FunctorInstanceMissingArgument {} -> Set.empty
       FunctorInstanceBadArgument {} -> Set.empty
       FunctorInstanceMissingName {} -> Set.empty
-      FunctorInstanceBadBacktickArgument {} -> Set.empty
+      FunctorInstanceBadBacktick {} -> Set.empty
 
       UnsupportedFFIKind {}  -> Set.empty
       UnsupportedFFIType _ t -> fvs t
@@ -567,14 +574,32 @@ instance PP (WithNames Error) where
               NSType      -> "type"
               NSModule    -> "module"
 
-      FunctorInstanceBadBacktickArgument i x ->
-        nested "Value parameter may not have a polymorphic type:" $
-          vcat
-            [ "Module parameter:" <+> pp i
-            , "Value parameter:" <+> pp x
-            , "When instantiatiating a functor using parameterization,"
-            , "the value parameters need to have a simple type."
-            ]
+      FunctorInstanceBadBacktick bad ->
+        case bad of
+          BIPolymorphicArgument i x ->
+            nested "Value parameter may not have a polymorphic type:" $
+              bullets
+                [ "Module parameter:" <+> pp i
+                , "Value parameter:" <+> pp x
+                , "When instantiatiating a functor using parameterization,"
+                  $$ "the value parameters need to have a simple type."
+                ]
+
+          BINested what ->
+            nested "Invalid declarations in parameterized instantiation:" $
+              bullets $
+                [ it <+> pp n
+                | (w,n) <- what
+                , let it = case w of
+                             BIFunctor -> "functor"
+                             BIInterface -> "interface"
+                             BIPrimitive -> "primitive"
+                             BIAbstractType -> "abstract type"
+                             BIForeign -> "foreign import"
+                ] ++
+                [ "A functor instantiated using parameterization," $$
+                  "may not contain nested functors, interfaces, or primitives."
+                ]
 
       UnsupportedFFIKind src param k ->
         nested "Kind of type variable unsupported for FFI: " $

src/Cryptol/TypeCheck/Module.hs

@@ -30,7 +30,7 @@ import Cryptol.TypeCheck.ModuleBacktickInstance(doBacktickInstance)
 
 doFunctorInst ::
   Located (P.ImpName Name)    {- ^ Name for the new module -} ->
-  Located (P.ImpName Name)    {- ^ Functor being instantiation -} ->
+  Located (P.ImpName Name)    {- ^ Functor being instantiated -} ->
   P.ModuleInstanceArgs Name   {- ^ Instance arguments -} ->
   Map Name Name
   {- ^ Instantitation.  These is the renaming for the functor that arises from
@@ -316,7 +316,8 @@ checkSimpleParameterValue r i mp =
     ([],[]) -> pure (Just (sType sch))
     _ ->
       do recordErrorLoc (Just r)
-            (FunctorInstanceBadBacktickArgument i (nameIdent (mvpName mp)))
+            (FunctorInstanceBadBacktick
+               (BIPolymorphicArgument i (nameIdent (mvpName mp))))
          pure Nothing
   where
   sch = mvpType mp