diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 2a4b2b1b..5879f753 100644 --- 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 index 04c8ca08..f21b7515 100644 --- 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 index 5154a3e2..5c8e4812 100644 --- 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