From 8470e250688668e65c7e14a3b06222bb9a6566d0 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 28 Jul 2020 15:41:08 -0700
Subject: [PATCH 1/3] Report many more unsolvable class constraints as
 `Unsolvable`. Also make the explanations/error messages a bit more uniform.
 Fixes #839.

---
 src/Cryptol/TypeCheck/Solver/Class.hs | 130 ++++++++++++++++++++++++--
 1 file changed, 121 insertions(+), 9 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
index c388c5d8f..f0ba0f13d 100644
--- a/src/Cryptol/TypeCheck/Solver/Class.hs
+++ b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -112,6 +112,26 @@ solveLogicInst ty = case tNoUser ty of
   -- Logic Bit
   TCon (TC TCBit) [] -> SolvedIf []
 
+  -- Logic Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support logical operations."
+
+  -- Logic (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support logical operations."
+
+  -- Logic Rational fails
+  TCon (TC TCRational) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Rational' does not support logical operations."
+
+  -- Logic (Float e p) fails
+  TCon (TC TCFloat) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Float' does not support logical operations."
+
   -- Logic a => Logic [n]a
   TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]
 
@@ -144,7 +164,7 @@ solveRingInst ty = case tNoUser ty of
 
   -- Ring Bit fails
   TCon (TC TCBit) [] ->
-    Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
+    Unsolvable $ TCErrorMessage "Type 'Bit' does not support ring operations."
 
   -- Ring Integer
   TCon (TC TCInteger) [] -> SolvedIf []
@@ -193,7 +213,7 @@ solveIntegralInst ty = case tNoUser ty of
 
   -- Integral Bit fails
   TCon (TC TCBit) [] ->
-    Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
+    Unsolvable $ TCErrorMessage "Type 'Bit' is not an integral type."
 
   -- Integral Integer
   TCon (TC TCInteger) [] -> SolvedIf []
@@ -219,6 +239,16 @@ solveFieldInst ty = case tNoUser ty of
   -- Field Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
+  -- Field Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support field operations."
+
+  -- Field Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support field operations."
+
   -- Field Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
@@ -226,9 +256,33 @@ solveFieldInst ty = case tNoUser ty of
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
   -- Field Real
-  -- Field (Z n)
+
+  -- Field (Z n) fails for now (to be added later with a 'prime n' requirement)
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support field operations."
 --  TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne, pPrime n ]
 
+  -- Field ([n]a) fails
+  TCon (TC TCSeq) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Sequence types do not support field operations."
+
+  -- Field (a -> b) fails
+  TCon (TC TCFun) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Function types do not support field operations."
+
+  -- Field (a, b, ...) fails
+  TCon (TC (TCTuple _)) _ ->
+    Unsolvable $
+    TCErrorMessage "Tuple types do not support field operations."
+
+  -- Field {x : a, y : b, ...} fails
+  TRec _ ->
+    Unsolvable $
+    TCErrorMessage "Record types do not support field operations."
+
   _ -> Unsolved
 
 
@@ -239,6 +293,21 @@ solveRoundInst ty = case tNoUser ty of
   -- Round Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
+  -- Round Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support rounding operations."
+
+  -- Round Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support rounding operations."
+
+  -- Round (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support rounding operations."
+
   -- Round Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
@@ -247,6 +316,26 @@ solveRoundInst ty = case tNoUser ty of
 
   -- Round Real
 
+  -- Round ([n]a) fails
+  TCon (TC TCSeq) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Sequence types do not support rounding operations."
+
+  -- Round (a -> b) fails
+  TCon (TC TCFun) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Function types do not support rounding operations."
+
+  -- Round (a, b, ...) fails
+  TCon (TC (TCTuple _)) _ ->
+    Unsolvable $
+    TCErrorMessage "Tuple types do not support rounding operations."
+
+  -- Round {x : a, y : b, ...} fails
+  TRec _ ->
+    Unsolvable $
+    TCErrorMessage "Record types do not support rounding operations."
+
   _ -> Unsolved
 
 
@@ -281,7 +370,7 @@ solveEqInst ty = case tNoUser ty of
 
   -- Eq (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
+    Unsolvable $ TCErrorMessage "Function types do not support comparisons."
 
   -- (Eq a, Eq b) => Eq { x:a, y:b }
   TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ]
@@ -307,7 +396,7 @@ solveCmpInst ty = case tNoUser ty of
 
   -- Cmp (Z n) fails
   TCon (TC TCIntMod) [_] ->
-    Unsolvable $ TCErrorMessage "Values of Z_n type cannot be compared for order"
+    Unsolvable $ TCErrorMessage "Type 'Z' does not support order comparisons."
 
   -- ValidFloat e p => Cmp (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
@@ -320,7 +409,7 @@ solveCmpInst ty = case tNoUser ty of
 
   -- Cmp (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
+    Unsolvable $ TCErrorMessage "Function types do not support order comparisons."
 
   -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
   TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ]
@@ -350,8 +439,30 @@ solveSignedCmpInst ty = case tNoUser ty of
   -- SignedCmp Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
-  -- SignedCmp Bit
-  TCon (TC TCBit) [] -> Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on bits"
+  -- SignedCmp Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support signed comparisons."
+
+  -- SignedCmp Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support signed comparisons."
+
+  -- SignedCmp (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support signed comparisons."
+
+  -- SignedCmp Rational fails
+  TCon (TC TCRational) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Rational' does not support signed comparisons."
+
+  -- SignedCmp (Float e p) fails
+  TCon (TC TCFloat) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Float' does not support signed comparisons."
 
   -- SignedCmp for sequences
   TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a
@@ -361,7 +472,8 @@ solveSignedCmpInst ty = case tNoUser ty of
 
   -- SignedCmp (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on functions."
+    Unsolvable $
+    TCErrorMessage "Function types do not support signed comparisons."
 
   -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
   TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ]

From 9c415a6a9703d01c6210eb5f68c612e96e7ab902 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 28 Jul 2020 15:43:59 -0700
Subject: [PATCH 2/3] Add regression test for all implicit instance rules in
 cryptol.

This includes a set of declarations in a file to test the rules
in the context of type checking. It also includes a set of type
queries to test the rules (or absence of rules) in the context
of type inference.
---
 tests/regression/instance.cry         | 365 +++++++++++++++++
 tests/regression/instance.icry        | 122 ++++++
 tests/regression/instance.icry.stdout | 543 ++++++++++++++++++++++++++
 3 files changed, 1030 insertions(+)
 create mode 100644 tests/regression/instance.cry
 create mode 100644 tests/regression/instance.icry
 create mode 100644 tests/regression/instance.icry.stdout

diff --git a/tests/regression/instance.cry b/tests/regression/instance.cry
new file mode 100644
index 000000000..9f3d0c1f2
--- /dev/null
+++ b/tests/regression/instance.cry
@@ -0,0 +1,365 @@
+module instance where
+
+////////////////////////////////////////////////////////////////////////////////
+//
+// This file includes a list of definitions intended to test all the
+// implicit class instance rules hard-wired into the Cryptol type
+// checker.
+
+import Float
+
+////////////////////////////////////////////////////////////////////////////////
+// Zero
+
+/** instance Zero Bit */
+zeroBit : Bit
+zeroBit = zero
+
+/** instance Zero Integer */
+zeroInteger : Integer
+zeroInteger = zero
+
+/** instance Zero Rational */
+zeroRational : Rational
+zeroRational = zero
+
+/** instance (fin n, n >= 1) => Zero (Z n) */
+zeroZ : {n} (fin n, n >= 1) => Z n
+zeroZ = zero
+
+/** instance Zero [n] */
+zeroWord : {n} [n]
+zeroWord = zero
+
+/** instance (Zero a) => Zero [n]a */
+zeroSeq : {n, a} (Zero a) => [n]a
+zeroSeq = zero
+
+/** instance (ValidFloat e p) => Zero (Float e p) */
+zeroFloat : {e, p} (ValidFloat e p) => Float e p
+zeroFloat = zero
+
+/** instance (Zero b) => Zero (a -> b) */
+zeroFun : {a, b} (Zero b) => a -> b
+zeroFun = zero
+
+/** instance Zero () */
+zeroUnit : ()
+zeroUnit = zero
+
+/** instance (Zero a, Zero b, ...) => Zero (a, b, ...) */
+zeroTuple : {a, b} (Zero a, Zero b) => (a, b)
+zeroTuple = zero
+
+/** instance Zero {} */
+zeroEmpty : {}
+zeroEmpty = zero
+
+/** instance (Zero a, Zero b, ...) => Zero { x : a, y : b, ... } */
+zeroRecord : {a, b} (Zero a, Zero b) => {x : a, y : b}
+zeroRecord = zero
+
+////////////////////////////////////////////////////////////////////////////////
+// Logic
+
+/** instance Logic Bit */
+logicBit : Bit -> Bit
+logicBit = complement
+
+/** instance Logic [n] */
+logicWord : {n} [n] -> [n]
+logicWord = complement
+
+/** instance (Logic a) => Logic [n]a */
+logicSeq : {n, a} (Logic a) => [n]a -> [n]a
+logicSeq = complement
+
+/** instance (Logic b) => Logic (a -> b) */
+logicFun : {a, b} (Logic b) => (a -> b) -> (a -> b)
+logicFun = complement
+
+/** instance Logic () */
+logicUnit : () -> ()
+logicUnit = complement
+
+/** instance (Logic a, Logic b, ...) => Logic (a, b, ...) */
+logicTuple : {a, b} (Logic a, Logic b) => (a, b) -> (a, b)
+logicTuple = complement
+
+/** instance Logic {} */
+logicEmpty : {} -> {}
+logicEmpty = complement
+
+/** instance (Logic a, Logic b, ...) => Logic { x : a, y : b, ... } */
+logicRecord : {a, b} (Logic a, Logic b) => {x : a, y : b} -> {x : a, y : b}
+logicRecord = complement
+
+////////////////////////////////////////////////////////////////////////////////
+// Ring
+
+/** instance Ring Integer */
+ringInteger : Integer -> Integer
+ringInteger = negate
+
+/** instance Ring Rational */
+ringRational : Rational -> Rational
+ringRational = negate
+
+/** instance (fin n, n >= 1) => Ring (Z n) */
+ringZ : {n} (fin n, n >= 1) => Z n -> Z n
+ringZ = negate
+
+/** instance (fin n) => Ring [n] */
+ringWord : {n} (fin n) => [n] -> [n]
+ringWord = negate
+
+// NOTE: 'instance Ring a => Ring [n]a' holds for any type 'a'
+// distinct from 'Bit'.
+
+/** instance Ring [n]Integer */
+ringSeqInteger : {n} [n]Integer -> [n]Integer
+ringSeqInteger = negate
+
+/** instance Ring [n]Rational */
+ringSeqRational : {n} [n]Rational -> [n]Rational
+ringSeqRational = negate
+
+/** instance (fin k, k >= 1) => Ring [n](Z k) */
+ringSeqZ : {n, k} (fin k, k >= 1) => [n](Z k) -> [n](Z k)
+ringSeqZ = negate
+
+/** instance (Ring [k]a) => Ring [n][k]a */
+ringSeqSeq : {n, k, a} (Ring ([k]a)) => [n][k]a -> [n][k]a
+ringSeqSeq = negate
+
+/** instance (Ring b) => Ring [n](a -> b) */
+ringSeqFun : {n, a, b} (Ring b) => [n](a -> b) -> [n](a -> b)
+ringSeqFun = negate
+
+/** instance Ring [n]() */
+ringSeqUnit : {n} [n]() -> [n]()
+ringSeqUnit = negate
+
+/** instance (Ring a, Ring b) => Ring [n](a, b) */
+ringSeqTuple : {n, a, b} (Ring a, Ring b) => [n](a, b) -> [n](a, b)
+ringSeqTuple = negate
+
+/** instance Ring [n]{} */
+ringSeqEmpty : {n} [n]{} -> [n]{}
+ringSeqEmpty = negate
+
+/** instance (Ring a, Ring b) => Ring [n]{x : a, y : b} */
+ringSeqRecord : {n, a, b} (Ring a, Ring b) => [n]{x : a, y : b} -> [n]{x : a, y : b}
+ringSeqRecord = negate
+
+/** instance (ValidFloat e p) => Ring (Float e p) */
+ringFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p
+ringFloat = negate
+
+/** instance (Ring b) => Ring (a -> b) */
+ringFun : {a, b} (Ring b) => (a -> b) -> (a -> b)
+ringFun = negate
+
+/** instance Ring () */
+ringUnit : () -> ()
+ringUnit = negate
+
+/** instance (Ring a, Ring b, ...) => Ring (a, b, ...) */
+ringTuple : {a, b} (Ring a, Ring b) => (a, b) -> (a, b)
+ringTuple = negate
+
+/** instance Ring {} */
+ringEmpty : {} -> {}
+ringEmpty = negate
+
+/** instance (Ring a, Ring b, ...) => Ring { x : a, y : b, ... } */
+ringRecord : {a, b} (Ring a, Ring b) => {x : a, y : b} -> {x : a, y : b}
+ringRecord = negate
+
+////////////////////////////////////////////////////////////////////////////////
+// Integral
+
+/** instance Integral Integer */
+integralInteger : Integer -> Integer -> Integer
+integralInteger = (%)
+
+/** instance (fin n) => Integral [n] */
+integralWord : {n} (fin n) => [n] -> [n] -> [n]
+integralWord = (%)
+
+////////////////////////////////////////////////////////////////////////////////
+// Field
+
+/** instance Field Rational */
+fieldRational : Rational -> Rational
+fieldRational = recip
+
+/** instance (ValidFloat e p) => Field (Float e p) */
+fieldFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p
+fieldFloat = recip
+
+////////////////////////////////////////////////////////////////////////////////
+// Round
+
+/** instance Round Rational */
+roundRational : Rational -> Integer
+roundRational = floor
+
+/** instance (ValidFloat e p) => Round (Float e p) */
+roundFloat : {e, p} (ValidFloat e p) => Float e p -> Integer
+roundFloat = floor
+
+////////////////////////////////////////////////////////////////////////////////
+// Eq
+
+/** instance Eq Bit */
+eqBit : Bit -> Bit -> Bit
+eqBit = (==)
+
+/** instance Eq Integer */
+eqInteger : Integer -> Integer -> Bit
+eqInteger = (==)
+
+/** instance Eq Rational */
+eqRational : Rational -> Rational -> Bit
+eqRational = (==)
+
+/** instance (fin n, n >= 1) => Eq (Z n) */
+eqZ : {n} (fin n, n >= 1) => Z n -> Z n -> Bit
+eqZ = (==)
+
+/** instance (fin n) => Eq [n] */
+eqWord : {n} (fin n) => [n] -> [n] -> Bit
+eqWord = (==)
+
+/** instance (fin n, Eq a) => Eq [n]a */
+eqSeq : {n, a} (fin n, Eq a) => [n]a -> [n]a -> Bit
+eqSeq = (==)
+
+/** instance (ValidFloat e p) => Eq (Float e p) */
+eqFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p -> Bit
+eqFloat = (==)
+
+/** instance Eq () */
+eqUnit : () -> () -> Bit
+eqUnit = (==)
+
+/** instance (Eq a, Eq b, ...) => Eq (a, b, ...) */
+eqTuple : {a, b} (Eq a, Eq b) => (a, b) -> (a, b) -> Bit
+eqTuple = (==)
+
+/** instance Eq {} */
+eqEmpty : {} -> {} -> Bit
+eqEmpty = (==)
+
+/** instance (Eq a, Eq b, ...) => Eq { x : a, y : b, ... } */
+eqRecord : {a, b} (Eq a, Eq b) => {x : a, y : b} ->  {x : a, y : b} -> Bit
+eqRecord = (==)
+
+////////////////////////////////////////////////////////////////////////////////
+// Cmp
+
+/** instance Cmp Bit */
+cmpBit : Bit -> Bit -> Bit
+cmpBit = (<)
+
+/** instance Cmp Integer */
+cmpInteger : Integer -> Integer -> Bit
+cmpInteger = (<)
+
+/** instance Cmp Rational */
+cmpRational : Rational -> Rational -> Bit
+cmpRational = (<)
+
+/** instance (fin n) => Cmp [n] */
+cmpWord : {n} (fin n) => [n] -> [n] -> Bit
+cmpWord = (<)
+
+/** instance (fin n, Cmp a) => Cmp [n]a */
+cmpSeq : {n, a} (fin n, Cmp a) => [n]a -> [n]a -> Bit
+cmpSeq = (<)
+
+/** instance (ValidFloat e p) => Cmp (Float e p) */
+cmpFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p -> Bit
+cmpFloat = (<)
+
+/** instance Cmp () */
+cmpUnit : () -> () -> Bit
+cmpUnit = (<)
+
+/** instance (Cmp a, Cmp b, ...) => Cmp (a, b, ...) */
+cmpTuple : {a, b} (Cmp a, Cmp b) => (a, b) -> (a, b) -> Bit
+cmpTuple = (<)
+
+/** instance Cmp {} */
+cmpEmpty : {} -> {} -> Bit
+cmpEmpty = (<)
+
+/** instance (Cmp a, Cmp b, ...) => Cmp { x : a, y : b, ... } */
+cmpRecord : {a, b} (Cmp a, Cmp b) => {x : a, y : b} ->  {x : a, y : b} -> Bit
+cmpRecord = (<)
+
+////////////////////////////////////////////////////////////////////////////////
+// Cmp
+
+/** instance (fin n, n >= 1) => SignedCmp [n] */
+signedCmpWord : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
+signedCmpWord = (<$)
+
+// NOTE: 'instance (fin n, SignedCmp a) => SignedCmp ([n]a)' holds for
+// any type 'a' distinct from 'Bit'.
+
+/** instance (fin n, SignedCmp [k]a) => SignedCmp [n][k]a */
+signedCmpSeqSeq : {n, k, a} (fin n, SignedCmp ([k]a)) => [n][k]a -> [n][k]a -> Bit
+signedCmpSeqSeq = (<$)
+
+/** instance (fin n) => SignedCmp [n]() */
+signedCmpSeqUnit : {n} (fin n) => [n]() -> [n]() -> Bit
+signedCmpSeqUnit = (<$)
+
+/** instance (SignedCmp a, SignedCmp b) => SignedCmp [n](a, b) */
+signedCmpSeqTuple : {n, a, b} (fin n, SignedCmp a, SignedCmp b) => [n](a, b) -> [n](a, b) -> Bit
+signedCmpSeqTuple = (<$)
+
+/** instance SignedCmp [n]{} */
+signedCmpSeqEmpty : {n} (fin n) => [n]{} -> [n]{} -> Bit
+signedCmpSeqEmpty = (<$)
+
+/** instance (SignedCmp a, SignedCmp b) => SignedCmp [n]{x : a, y : b} */
+signedCmpSeqRecord : {n, a, b} (fin n, SignedCmp a, SignedCmp b) => [n]{x : a, y : b} -> [n]{x : a, y : b} -> Bit
+signedCmpSeqRecord = (<$)
+
+/** instance SignedCmp () */
+signedCmpUnit : () -> () -> Bit
+signedCmpUnit = (<$)
+
+/** instance (SignedCmp a, SignedCmp b, ...) => SignedCmp (a, b, ...) */
+signedCmpTuple : {a, b} (SignedCmp a, SignedCmp b) => (a, b) -> (a, b) -> Bit
+signedCmpTuple = (<$)
+
+/** instance SignedCmp {} */
+signedCmpEmpty : {} -> {} -> Bit
+signedCmpEmpty = (<$)
+
+/** instance (SignedCmp a, SignedCmp b, ...) => SignedCmp { x : a, y : b, ... } */
+signedCmpRecord : {a, b} (SignedCmp a, SignedCmp b) => {x : a, y : b} ->  {x : a, y : b} -> Bit
+signedCmpRecord = (<$)
+
+////////////////////////////////////////////////////////////////////////////////
+// Literal
+
+/** instance (fin val) => Literal val Integer */
+literalInteger : {val} (fin val) => Integer
+literalInteger = `val
+
+/** instance (fin val) => Literal val Rational */
+literalRational : {val} (fin val) => Rational
+literalRational = `val
+
+/** instance (fin val, fin n, n >= 1, n > val) => Literal val (Z n) */
+literalZ : {val, n} (fin val, fin n, n >= 1, n > val) => Z n
+literalZ = `val
+
+/** instance (fin val, fin n, n >= width val) => Literal val [n] */
+literalWord : {val, n} (fin val, fin n, n >= width val) => [n]
+literalWord = `val
diff --git a/tests/regression/instance.icry b/tests/regression/instance.icry
new file mode 100644
index 000000000..d669cb7bb
--- /dev/null
+++ b/tests/regression/instance.icry
@@ -0,0 +1,122 @@
+:l instance.cry
+
+:t zero`{Bit}
+:t zero`{Integer}
+:t zero`{Rational}
+:t zero`{Z _}
+:t zero`{[_]_}
+:t zero`{_ -> _}
+:t zero`{()}
+:t zero`{(_, _)}
+:t zero`{{}}
+:t zero`{{x : _, y : _}}
+:t zero`{Float _ _}
+
+:t complement`{Bit}
+:t complement`{Integer}
+:t complement`{Rational}
+:t complement`{Z _}
+:t complement`{[_]_}
+:t complement`{(_ -> _)}
+:t complement`{()}
+:t complement`{(_, _)}
+:t complement`{{}}
+:t complement`{{x : _, y : _}}
+:t complement`{Float _ _}
+
+:t negate`{Bit}
+:t negate`{Integer}
+:t negate`{Rational}
+:t negate`{Z _}
+:t negate`{[_]}
+:t negate`{[_]_}
+:t negate`{(_ -> _)}
+:t negate`{()}
+:t negate`{(_, _)}
+:t negate`{{}}
+:t negate`{{x : _, y : _}}
+:t negate`{Float _ _}
+
+:t (%)`{Bit}
+:t (%)`{Integer}
+:t (%)`{Rational}
+:t (%)`{Z _}
+:t (%)`{[_]_}
+:t (%)`{(_ -> _)}
+:t (%)`{()}
+:t (%)`{(_, _)}
+:t (%)`{{}}
+:t (%)`{{x : _, y : _}}
+:t (%)`{Float _ _}
+
+:t recip`{Bit}
+:t recip`{Integer}
+:t recip`{Rational}
+:t recip`{Z _}
+:t recip`{[_]_}
+:t recip`{(_ -> _)}
+:t recip`{()}
+:t recip`{(_, _)}
+:t recip`{{}}
+:t recip`{{x : _, y : _}}
+:t recip`{Float _ _}
+
+:t floor`{Bit}
+:t floor`{Integer}
+:t floor`{Rational}
+:t floor`{Z _}
+:t floor`{[_]_}
+:t floor`{(_ -> _)}
+:t floor`{()}
+:t floor`{(_, _)}
+:t floor`{{}}
+:t floor`{{x : _, y : _}}
+:t floor`{Float _ _}
+
+:t (==)`{Bit}
+:t (==)`{Integer}
+:t (==)`{Rational}
+:t (==)`{Z _}
+:t (==)`{[_]_}
+:t (==)`{(_ -> _)}
+:t (==)`{()}
+:t (==)`{(_, _)}
+:t (==)`{{}}
+:t (==)`{{x : _, y : _}}
+:t (==)`{Float _ _}
+
+:t (<)`{Bit}
+:t (<)`{Integer}
+:t (<)`{Rational}
+:t (<)`{Z _}
+:t (<)`{[_]_}
+:t (<)`{(_ -> _)}
+:t (<)`{()}
+:t (<)`{(_, _)}
+:t (<)`{{}}
+:t (<)`{{x : _, y : _}}
+:t (<)`{Float _ _}
+
+:t (<$)`{Bit}
+:t (<$)`{Integer}
+:t (<$)`{Rational}
+:t (<$)`{Z _}
+:t (<$)`{[_]_}
+:t (<$)`{(_ -> _)}
+:t (<$)`{()}
+:t (<$)`{(_, _)}
+:t (<$)`{{}}
+:t (<$)`{{x : _, y : _}}
+:t (<$)`{Float _ _}
+
+:t number`{rep = Bit}
+:t number`{rep = Integer}
+:t number`{rep = Rational}
+:t number`{rep = Z _}
+:t number`{rep = [_]_}
+:t number`{rep = _ -> _}
+:t number`{rep = ()}
+:t number`{rep = (_, _)}
+:t number`{rep = {}}
+:t number`{rep = {x : _, y : _}}
+:t number`{rep = Float _ _}
diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout
new file mode 100644
index 000000000..c2a52ada1
--- /dev/null
+++ b/tests/regression/instance.icry.stdout
@@ -0,0 +1,543 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Float
+Loading module instance
+zero`{Bit} : Bit
+zero`{Integer} : Integer
+zero`{Rational} : Rational
+zero`{Z _} : {n} (n >= 1, fin n) => Z n
+zero`{[_]_} : {n, a} (Zero a) => [n]a
+zero`{_ -> _} : {a, b} (Zero b) => a -> b
+zero`{()} : ()
+zero`{(_, _)} : {a, b} (Zero b, Zero a) => (a, b)
+zero`{{}} : {}
+zero`{{x : _, y : _}} : {a, b} (Zero b, Zero a) => {x : a, y : b}
+zero`{Float _ _} : {n, m} (ValidFloat n m) => Float n m
+complement`{Bit} : Bit -> Bit
+
+[error] at <interactive>:1:1--1:11:
+  Unsolvable constraints:
+    • Logic Integer
+        arising from
+        use of expression complement
+        at <interactive>:1:1--1:11
+    • Reason: Type 'Integer' does not support logical operations.
+
+[error] at <interactive>:1:1--1:11:
+  Unsolvable constraints:
+    • Logic Rational
+        arising from
+        use of expression complement
+        at <interactive>:1:1--1:11
+    • Reason: Type 'Rational' does not support logical operations.
+
+[error] at <interactive>:1:1--1:11:
+  Unsolvable constraints:
+    • Logic (Z ?n`1179)
+        arising from
+        use of expression complement
+        at <interactive>:1:1--1:11
+    • Reason: Type 'Z' does not support logical operations.
+  where
+  ?n`1179 is type wildcard (_) at <interactive>:1:15--1:16
+complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a
+complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b
+complement`{()} : () -> ()
+complement`{(_, _)} : {a, b} (Logic b, Logic a) => (a, b) -> (a, b)
+complement`{{}} : {} -> {}
+complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) =>
+                                {x : a, y : b} -> {x : a, y : b}
+
+[error] at <interactive>:1:1--1:11:
+  Unsolvable constraints:
+    • Logic (Float ?n`1193 ?n`1194)
+        arising from
+        use of expression complement
+        at <interactive>:1:1--1:11
+    • Reason: Type 'Float' does not support logical operations.
+  where
+  ?n`1193 is type wildcard (_) at <interactive>:1:19--1:20
+  ?n`1194 is type wildcard (_) at <interactive>:1:21--1:22
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Ring Bit
+        arising from
+        use of expression negate
+        at <interactive>:1:1--1:7
+    • Reason: Type 'Bit' does not support ring operations.
+negate`{Integer} : Integer -> Integer
+negate`{Rational} : Rational -> Rational
+negate`{Z _} : {n} (n >= 1, fin n) => Z n -> Z n
+negate`{[_]} : {n} (fin n) => [n] -> [n]
+negate`{[_]_} : {n, a} (Ring ([n]a)) => [n]a -> [n]a
+negate`{(_ -> _)} : {a, b} (Ring b) => (a -> b) -> a -> b
+negate`{()} : () -> ()
+negate`{(_, _)} : {a, b} (Ring b, Ring a) => (a, b) -> (a, b)
+negate`{{}} : {} -> {}
+negate`{{x : _, y : _}} : {a, b} (Ring b, Ring a) =>
+                            {x : a, y : b} -> {x : a, y : b}
+negate`{Float _ _} : {n, m} (ValidFloat n m) =>
+                       Float n m -> Float n m
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral Bit
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type 'Bit' is not an integral type.
+(%)`{Integer} : Integer -> Integer -> Integer
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral Rational
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type 'Rational' is not an integral type.
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral (Z ?n`1217)
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type 'Z ?n`1217' is not an integral type.
+  where
+  ?n`1217 is type wildcard (_) at <interactive>:1:8--1:9
+(%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral (?a`1220 -> ?a`1221)
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type '?a`1220 -> ?a`1221' is not an integral type.
+  where
+  ?a`1220 is type wildcard (_) at <interactive>:1:7--1:8
+  ?a`1221 is type wildcard (_) at <interactive>:1:12--1:13
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral ()
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type '()' is not an integral type.
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral (?a`1220, ?a`1221)
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type '(?a`1220, ?a`1221)' is not an integral type.
+  where
+  ?a`1220 is type wildcard (_) at <interactive>:1:7--1:8
+  ?a`1221 is type wildcard (_) at <interactive>:1:10--1:11
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral {}
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type '{}' is not an integral type.
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral {x : ?a`1220, y : ?a`1221}
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type '{x : ?a`1220, y : ?a`1221}' is not an integral type.
+  where
+  ?a`1220 is type wildcard (_) at <interactive>:1:11--1:12
+  ?a`1221 is type wildcard (_) at <interactive>:1:18--1:19
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Integral (Float ?n`1220 ?n`1221)
+        arising from
+        use of expression (%)
+        at <interactive>:1:1--1:4
+    • Reason: Type 'Float ?n`1220 ?n`1221' is not an integral type.
+  where
+  ?n`1220 is type wildcard (_) at <interactive>:1:12--1:13
+  ?n`1221 is type wildcard (_) at <interactive>:1:14--1:15
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field Bit
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Bit' does not support field operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field Integer
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Integer' does not support field operations.
+recip`{Rational} : Rational -> Rational
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field (Z ?n`1221)
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Z' does not support field operations.
+  where
+  ?n`1221 is type wildcard (_) at <interactive>:1:10--1:11
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field ([?n`1221]?a`1222)
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Sequence types do not support field operations.
+  where
+  ?n`1221 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1222 is type wildcard (_) at <interactive>:1:11--1:12
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field (?a`1221 -> ?a`1222)
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Function types do not support field operations.
+  where
+  ?a`1221 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1222 is type wildcard (_) at <interactive>:1:14--1:15
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field ()
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Tuple types do not support field operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field (?a`1221, ?a`1222)
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Tuple types do not support field operations.
+  where
+  ?a`1221 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1222 is type wildcard (_) at <interactive>:1:12--1:13
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field {}
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Record types do not support field operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Field {x : ?a`1221, y : ?a`1222}
+        arising from
+        use of expression recip
+        at <interactive>:1:1--1:6
+    • Reason: Record types do not support field operations.
+  where
+  ?a`1221 is type wildcard (_) at <interactive>:1:13--1:14
+  ?a`1222 is type wildcard (_) at <interactive>:1:20--1:21
+recip`{Float _ _} : {n, m} (ValidFloat n m) =>
+                      Float n m -> Float n m
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round Bit
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Bit' does not support rounding operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round Integer
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Integer' does not support rounding operations.
+floor`{Rational} : Rational -> Integer
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round (Z ?n`1225)
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Type 'Z' does not support rounding operations.
+  where
+  ?n`1225 is type wildcard (_) at <interactive>:1:10--1:11
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round ([?n`1225]?a`1226)
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Sequence types do not support rounding operations.
+  where
+  ?n`1225 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1226 is type wildcard (_) at <interactive>:1:11--1:12
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round (?a`1225 -> ?a`1226)
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Function types do not support rounding operations.
+  where
+  ?a`1225 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1226 is type wildcard (_) at <interactive>:1:14--1:15
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round ()
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Tuple types do not support rounding operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round (?a`1225, ?a`1226)
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Tuple types do not support rounding operations.
+  where
+  ?a`1225 is type wildcard (_) at <interactive>:1:9--1:10
+  ?a`1226 is type wildcard (_) at <interactive>:1:12--1:13
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round {}
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Record types do not support rounding operations.
+
+[error] at <interactive>:1:1--1:6:
+  Unsolvable constraints:
+    • Round {x : ?a`1225, y : ?a`1226}
+        arising from
+        use of expression floor
+        at <interactive>:1:1--1:6
+    • Reason: Record types do not support rounding operations.
+  where
+  ?a`1225 is type wildcard (_) at <interactive>:1:13--1:14
+  ?a`1226 is type wildcard (_) at <interactive>:1:20--1:21
+floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
+(==)`{Bit} : Bit -> Bit -> Bit
+(==)`{Integer} : Integer -> Integer -> Bit
+(==)`{Rational} : Rational -> Rational -> Bit
+(==)`{Z _} : {n} (n >= 1, fin n) => Z n -> Z n -> Bit
+(==)`{[_]_} : {n, a} (Eq a, fin n) => [n]a -> [n]a -> Bit
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • Eq (?a`1236 -> ?a`1237)
+        arising from
+        use of expression (==)
+        at <interactive>:1:1--1:5
+    • Reason: Function types do not support comparisons.
+  where
+  ?a`1236 is type wildcard (_) at <interactive>:1:8--1:9
+  ?a`1237 is type wildcard (_) at <interactive>:1:13--1:14
+(==)`{()} : () -> () -> Bit
+(==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit
+(==)`{{}} : {} -> {} -> Bit
+(==)`{{x : _, y : _}} : {a, b} (Eq b, Eq a) =>
+                          {x : a, y : b} -> {x : a, y : b} -> Bit
+(==)`{Float _ _} : {n, m} (ValidFloat n m) =>
+                     Float n m -> Float n m -> Bit
+(<)`{Bit} : Bit -> Bit -> Bit
+(<)`{Integer} : Integer -> Integer -> Bit
+(<)`{Rational} : Rational -> Rational -> Bit
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Cmp (Z ?n`1250)
+        arising from
+        use of expression (<)
+        at <interactive>:1:1--1:4
+    • Reason: Type 'Z' does not support order comparisons.
+  where
+  ?n`1250 is type wildcard (_) at <interactive>:1:8--1:9
+(<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit
+
+[error] at <interactive>:1:1--1:4:
+  Unsolvable constraints:
+    • Cmp (?a`1253 -> ?a`1254)
+        arising from
+        use of expression (<)
+        at <interactive>:1:1--1:4
+    • Reason: Function types do not support order comparisons.
+  where
+  ?a`1253 is type wildcard (_) at <interactive>:1:7--1:8
+  ?a`1254 is type wildcard (_) at <interactive>:1:12--1:13
+(<)`{()} : () -> () -> Bit
+(<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit
+(<)`{{}} : {} -> {} -> Bit
+(<)`{{x : _, y : _}} : {a, b} (Cmp b, Cmp a) =>
+                         {x : a, y : b} -> {x : a, y : b} -> Bit
+(<)`{Float _ _} : {n, m} (ValidFloat n m) =>
+                    Float n m -> Float n m -> Bit
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp Bit
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Type 'Bit' does not support signed comparisons.
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp Integer
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Type 'Integer' does not support signed comparisons.
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp Rational
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Type 'Rational' does not support signed comparisons.
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp (Z ?n`1264)
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Type 'Z' does not support signed comparisons.
+  where
+  ?n`1264 is type wildcard (_) at <interactive>:1:9--1:10
+(<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp (?a`1267 -> ?a`1268)
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Function types do not support signed comparisons.
+  where
+  ?a`1267 is type wildcard (_) at <interactive>:1:8--1:9
+  ?a`1268 is type wildcard (_) at <interactive>:1:13--1:14
+(<$)`{()} : () -> () -> Bit
+(<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) =>
+                  (a, b) -> (a, b) -> Bit
+(<$)`{{}} : {} -> {} -> Bit
+(<$)`{{x : _, y : _}} : {a, b} (SignedCmp b, SignedCmp a) =>
+                          {x : a, y : b} -> {x : a, y : b} -> Bit
+
+[error] at <interactive>:1:1--1:5:
+  Unsolvable constraints:
+    • SignedCmp (Float ?n`1275 ?n`1276)
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:5
+    • Reason: Type 'Float' does not support signed comparisons.
+  where
+  ?n`1275 is type wildcard (_) at <interactive>:1:13--1:14
+  ?n`1276 is type wildcard (_) at <interactive>:1:15--1:16
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1275 Bit
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type 'Bit' does not support integer literals.
+  where
+  ?val`1275 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+
+[error] at <interactive>:1:1--1:7:
+  Ambiguous numeric type: type argument 'val' of 'number'
+
+[error] at <interactive>:1:1--1:7:
+  Ambiguous numeric type: type argument 'val' of 'number'
+number`{rep = Z _} : {n, m} (m >= 1 + n, m >= 1, fin m, fin n) =>
+                       Z m
+number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m]
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1282 (?a`1283 -> ?a`1284)
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type '?a`1283 -> ?a`1284' does not support integer literals.
+  where
+  ?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+  ?a`1283 is type wildcard (_) at <interactive>:1:15--1:16
+  ?a`1284 is type wildcard (_) at <interactive>:1:20--1:21
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1282 ()
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type '()' does not support integer literals.
+  where
+  ?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1282 (?a`1283, ?a`1284)
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type '(?a`1283, ?a`1284)' does not support integer literals.
+  where
+  ?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+  ?a`1283 is type wildcard (_) at <interactive>:1:16--1:17
+  ?a`1284 is type wildcard (_) at <interactive>:1:19--1:20
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1282 {}
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type '{}' does not support integer literals.
+  where
+  ?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+
+[error] at <interactive>:1:1--1:7:
+  Unsolvable constraints:
+    • Literal ?val`1282 {x : ?a`1283, y : ?a`1284}
+        arising from
+        use of literal or demoted expression
+        at <interactive>:1:1--1:7
+    • Reason: Type '{x : ?a`1283,
+       y : ?a`1284}' does not support integer literals.
+  where
+  ?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
+  ?a`1283 is type wildcard (_) at <interactive>:1:20--1:21
+  ?a`1284 is type wildcard (_) at <interactive>:1:27--1:28
+number`{rep = Float _ _} : {n, m, i} (ValidFloat m i,
+                                      Literal n (Float m i)) =>
+                             Float m i

From fe465e108f45e361df7d869f9cd7f6f2956db21f Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 28 Jul 2020 16:03:20 -0700
Subject: [PATCH 3/3] Update expected output for regression test issue835.icry.

---
 tests/issues/issue835.icry.stdout | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/issues/issue835.icry.stdout b/tests/issues/issue835.icry.stdout
index da04b3e2e..6e6137910 100644
--- a/tests/issues/issue835.icry.stdout
+++ b/tests/issues/issue835.icry.stdout
@@ -3,8 +3,9 @@ Loading module Cryptol
 Loading module Float
 
 [error] at <interactive>:1:1--1:28:
-  Unsolved constraints:
+  Unsolvable constraints:
     • SignedCmp (Float 5 11)
         arising from
         use of expression (<$)
         at <interactive>:1:1--1:28
+    • Reason: Type 'Float' does not support signed comparisons.