Check that the declared type of prims matches the expected one.

Fixes #711
GaloisInc · May 5, 2020 · c3eca4f · c3eca4f
1 parent 6adec7f
commit c3eca4f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 3 deletions.
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
@@ -57,7 +57,7 @@ primitive type (!=) : # -> # -> Prop
 primitive type (>=) : # -> # -> Prop
 
 /** Assert that a numeric type is a proper natural number (not 'inf'). */
-primitive type fin : * -> Prop
+primitive type fin : # -> Prop
 
 /** Value types that have a notion of 'zero'. */
 primitive type Zero : * -> Prop

diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
@@ -292,7 +292,15 @@ newtypeConType nt =
 abstractTypeTC :: AbstractType -> TCon
 abstractTypeTC at =
   case builtInType (atName at) of
-    Just tcon -> tcon
+    Just tcon
+      | kindOf tcon == atKind at -> tcon
+      | otherwise ->
+        panic "abstractTypeTC"
+          [ "Mismatch between built-in and declared type."
+          , "Name: " ++ pretty (atName at)
+          , "Declared: " ++ pretty (atKind at)
+          , "Built-in: " ++ pretty (kindOf tcon)
+          ]
     _         -> TC $ TCAbstract $ UserTC (atName at) (atKind at)
 
 instance Eq TVar where

diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout
@@ -44,7 +44,7 @@ Primitive Types
     Arith : * -> Prop
     Bit : *
     Cmp : * -> Prop
-    fin : * -> Prop
+    fin : # -> Prop
     Integer : *
     inf : #
     Literal : # -> * -> Prop