Add inequality constraints to types of fromThen and fromThenTo.

This ensures that all applications of partial type functions are
well-defined.

Fixes #416.

lib/Cryptol.cry

@@ -456,6 +456,7 @@ updatesEnd xs0 idxs vals = xss!0
 primitive fromThen : {first, next, bits, len}
                      ( fin first, fin next, fin bits
                      , bits >= width first, bits >= width next
+                     , first != next
                      , lengthFromThen first next bits == len) => [len][bits]
 
 /**
@@ -475,6 +476,7 @@ primitive fromTo : {first, last, a} (fin last, last >= first, Literal last a) =>
 primitive fromThenTo : {first, next, last, a, len}
                        ( fin first, fin next, fin last
                        , Literal first a, Literal next a, Literal last a
+                       , first != next
                        , lengthFromThenTo first next last == len) => [len]a
 
 /**

tests/issues/issue226.icry.stdout

@@ -67,12 +67,12 @@ Symbols
     fromInteger : {a} (Arith a) => Integer -> a
     fromThen :
       {first, next, bits, len} (fin first, fin next, fin bits,
-                                bits >= width first, bits >= width next,
+                                bits >= width first, bits >= width next, first != next,
                                 lengthFromThen first next bits == len) =>
         [len][bits]
     fromThenTo :
       {first, next, last, a, len} (fin first, fin next, fin last,
-                                   Literal first a, Literal next a, Literal last a,
+                                   Literal first a, Literal next a, Literal last a, first != next,
                                    lengthFromThenTo first next last == len) =>
         [len]a
     fromTo :

tests/issues/issue416.cry

@@ -0,0 +1,5 @@
+f : {n} (fin n, 3 >= width n) => [lengthFromThenTo 1 n 7][3]
+f = [1, n .. 7]
+
+g : {n} (fin n, 3 >= width n) => [_][3]
+g = [1, n .. 7]

tests/issues/issue416.icry

@@ -0,0 +1 @@
+:l issue416.cry

tests/issues/issue416.icry.stdout

@@ -0,0 +1,26 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at ./issue416.cry:2:1--2:16:
+  Failed to validate user-specified signature.
+    In the definition of 'Main::f', at ./issue416.cry:2:1--2:2:
+      for any type n
+        fin n
+        3 >= width n
+      =>
+      1 != n
+        arising from
+        use of partial type function lengthFromThenTo
+        at ./issue416.cry:1:5--1:61
+[error] at ./issue416.cry:5:1--5:16:
+  Failed to validate user-specified signature.
+    In the definition of 'Main::g', at ./issue416.cry:5:1--5:2:
+      for any type n
+        fin n
+        3 >= width n
+      =>
+      1 != n
+        arising from
+        use of finite enumeration
+        at ./issue416.cry:5:5--5:16