From 19630f8cf7d1f7f1a1ab9762588dee0cbdf04acb Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Wed, 10 Feb 2021 12:02:48 -0800
Subject: [PATCH] Demote the `panic` that arises from bare type applications to
 a kind-checking error.  This at least provides actionable feedback about
 where the error occurs.

We should also improve the parser post-processing pass to
handle these situations better, but this at least removes
the panic.
---
 src/Cryptol/TypeCheck/Error.hs | 10 ++++++++++
 src/Cryptol/TypeCheck/Kind.hs  |  4 ++--
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs
index 3ce356135..3db3009fd 100644
--- a/src/Cryptol/TypeCheck/Error.hs
+++ b/src/Cryptol/TypeCheck/Error.hs
@@ -128,6 +128,9 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
                 --   but we know it must be at least as large as the given type
                 --   (or unconstrained, if Nothing).
 
+              | BareTypeApp
+                -- ^ Bare expression of the form `{_}
+
               | UndefinedExistVar Name
               | TypeShadowing String Name String
               | MissingModTParam (Located Ident)
@@ -139,6 +142,7 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
 errorImportance :: Error -> Int
 errorImportance err =
   case err of
+    BareTypeApp{}                                    -> 11 -- basically a parse error
     KindMismatch {}                                  -> 10
     TyVarWithParams {}                               -> 9
     TypeMismatch {}                                  -> 8
@@ -180,6 +184,7 @@ errorImportance err =
 
 
 
+
 instance TVars Warning where
   apSubst su warn =
     case warn of
@@ -219,6 +224,7 @@ instance TVars Error where
       RepeatedTypeParameter {} -> err
       AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t)
 
+      BareTypeApp{} -> err
 
       UndefinedExistVar {} -> err
       TypeShadowing {}     -> err
@@ -250,6 +256,8 @@ instance FVS Error where
       RepeatedTypeParameter {}              -> Set.empty
       AmbiguousSize _ t -> fvs t
 
+      BareTypeApp{} -> Set.empty
+
       UndefinedExistVar {} -> Set.empty
       TypeShadowing {}     -> Set.empty
       MissingModTParam {}  -> Set.empty
@@ -403,6 +411,8 @@ instance PP (WithNames Error) where
                  Nothing -> empty
          in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg)
 
+      BareTypeApp -> "Unexpected bare type application"
+
       UndefinedExistVar x -> "Undefined type" <+> quotes (pp x)
       TypeShadowing this new that ->
         "Type" <+> text this <+> quotes (pp new) <+>
diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs
index 30cf7a1f9..8b8012a09 100644
--- a/src/Cryptol/TypeCheck/Kind.hs
+++ b/src/Cryptol/TypeCheck/Kind.hs
@@ -387,8 +387,8 @@ doCheckType ty k =
 
     P.TInfix t x _ u-> doCheckType (P.TUser (thing x) [t, u]) k
 
-    P.TTyApp _fs    -> panic "doCheckType"
-                         ["TTyApp found when kind checking, but it should have been eliminated already"]
+    P.TTyApp _fs    -> do kRecordError BareTypeApp
+                          kNewType TypeWildCard KNum
 
   where
   checkF _nm (rng,v) = kInRange rng $ doCheckType v (Just KType)