Complain when we spot invalid literals. Fixes #519

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -8,7 +8,7 @@
 --
 -- Solving class constraints.
 
-{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternGuards, OverloadedStrings #-}
 module Cryptol.TypeCheck.Solver.Class
   ( classStep
   , solveZeroInst
@@ -23,6 +23,7 @@ module Cryptol.TypeCheck.Solver.Class
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.SimpType (tAdd,tWidth)
 import Cryptol.TypeCheck.Solver.Types
+import Cryptol.TypeCheck.PP
 
 -- | Solve class constraints.
 -- If not, then we return 'Nothing'.
@@ -225,10 +226,16 @@ solveLiteralInst val ty
         SolvedIf [ pFin val, pFin modulus, modulus >== tAdd val tOne ]
 
       -- (fin bits, bits => width n) => Literal n [bits]
-      TCon (TC TCSeq) [bits, TCon (TC TCBit) []] ->
-        SolvedIf [ pFin val, pFin bits, bits >== tWidth val ]
+      TCon (TC TCSeq) [bits, elTy]
+        | TCon (TC TCBit) [] <- ety ->
+            SolvedIf [ pFin val, pFin bits, bits >== tWidth val ]
+        | TVar _ <- ety -> Unsolved
+        where ety = tNoUser elTy
 
-      _ -> Unsolved
+      TVar _ -> Unsolved
+
+      _ -> Unsolvable $ TCErrorMessage $ show
+         $ "Type" <+> quotes (pp ty) <+> "does not support literals."
 
 
 -- | Add propositions that are implied by the given one.

tests/mono-binds/test04.icry.stdout

@@ -17,9 +17,5 @@ test04::test = \{a, b} (Literal 10 b) (a : a) ->
 Loading module Cryptol
 Loading module test04
 
-[error] at ./test04.cry:3:19--3:21:
-  Unsolved constraints:
-    Literal 10 ()
-      arising from
-      use of literal or demoted expression
-      at ./test04.cry:3:19--3:21
+[error] at ./test04.cry:1:1--5:14:
+  Type '()' does not support literals.