Tweak error messages

docs/RefMan/TypeDeclarations.rst

@@ -163,8 +163,9 @@ constructor:
     case x of
       Nothing -> True
 
-**The Matched Expression Must Have an Unambiguous Type.** Cryptol will reject
-the definition of ``f``, where ``f`` lacks a type signature:
+**The Matched Expression Must Have a Knwon Enum Type.** Cryptol will reject
+the definition of ``f``, where ``f`` lacks a type signature, or is not not
+an ``enum`` type.
 
 .. code-block:: cryptol
 

docs/RefMan/_build/html/RefMan.html

@@ -128,7 +128,7 @@ <h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manua
 <li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a><ul>
 <li class="toctree-l2"><a class="reference internal" href="TypeDeclarations.html#type-synonyms">Type Synonyms</a></li>
 <li class="toctree-l2"><a class="reference internal" href="TypeDeclarations.html#newtypes">Newtypes</a></li>
-<li class="toctree-l2"><a class="reference internal" href="TypeDeclarations.html#enumerations">Enumerations</a></li>
+<li class="toctree-l2"><a class="reference internal" href="TypeDeclarations.html#enums">Enums</a></li>
 </ul>
 </li>
 <li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a><ul>

docs/RefMan/_build/html/TypeDeclarations.html

@@ -49,7 +49,7 @@
 <li class="toctree-l1 current"><a class="current reference internal" href="#">Type Declarations</a><ul>
 <li class="toctree-l2"><a class="reference internal" href="#type-synonyms">Type Synonyms</a></li>
 <li class="toctree-l2"><a class="reference internal" href="#newtypes">Newtypes</a></li>
-<li class="toctree-l2"><a class="reference internal" href="#enumerations">Enumerations</a></li>
+<li class="toctree-l2"><a class="reference internal" href="#enums">Enums</a></li>
 </ul>
 </li>
 <li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
@@ -124,16 +124,17 @@ <h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this head
 </pre></div>
 </div>
 </section>
-<section id="enumerations">
-<h2>Enumerations<a class="headerlink" href="#enumerations" title="Permalink to this heading"></a></h2>
+<section id="enums">
+<h2>Enums<a class="headerlink" href="#enums" title="Permalink to this heading"></a></h2>
 <div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">enum</span><span class="w"> </span><span class="kt">Maybe</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kt">Nothing</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="kt">Just</span><span class="w"> </span><span class="n">a</span>
 </pre></div>
 </div>
-<p>An <code class="docutils literal notranslate"><span class="pre">enum</span></code> declaration introduces a new named type, which is defined by
-a collection of <em>constructors</em>.  Each named <code class="docutils literal notranslate"><span class="pre">enum</span></code> type is treated like
-a separate type, even if it has the exact same constructors as another <code class="docutils literal notranslate"><span class="pre">enum</span></code>
-type—in this way <code class="docutils literal notranslate"><span class="pre">enum</span></code> is similar to <code class="docutils literal notranslate"><span class="pre">newtype</span></code> and unlike <code class="docutils literal notranslate"><span class="pre">type</span></code>
-synonyms.</p>
+<p>An <code class="docutils literal notranslate"><span class="pre">enum</span></code> declaration introduces a new named type, which is defined by a
+collection of <em>constructors</em>. <code class="docutils literal notranslate"><span class="pre">enum</span></code> declarations correspond to the notion of
+<em>algebraic data types</em>, which are commonly found in other programming
+languages. Each named <code class="docutils literal notranslate"><span class="pre">enum</span></code> type is treated like a separate type, even if it
+has the exact same constructors as another <code class="docutils literal notranslate"><span class="pre">enum</span></code> type—in this way <code class="docutils literal notranslate"><span class="pre">enum</span></code>
+is similar to <code class="docutils literal notranslate"><span class="pre">newtype</span></code> and unlike <code class="docutils literal notranslate"><span class="pre">type</span></code> synonyms.</p>
 <p><strong>Constructors.</strong> The only way to create a value of an <code class="docutils literal notranslate"><span class="pre">enum</span></code> type is to
 use one of its constructors.   When used in an expression, the constructors
 behave like an ordinary function, which has one parameter for each field of the
@@ -182,10 +183,63 @@ <h2>Enumerations<a class="headerlink" href="#enumerations" title="Permalink to t
 as long as this type does not depend on the type to which the constructor
 belongs.  This means that we do not support defining recursive types,
 such as linked lists.</p>
-<p><strong>No Nested Consturctor Patterns.</strong>  For simplicity, only non-constructor
+<p><strong>No Nested Constructor Patterns.</strong>  For simplicity, only non-constructor
 patterns may be used in the fields of a constructor pattern.  For example,
 <code class="docutils literal notranslate"><span class="pre">Just</span> <span class="pre">(a,b)</span></code> and <code class="docutils literal notranslate"><span class="pre">Just</span> <span class="pre">(a</span> <span class="pre">#</span> <span class="pre">b)</span></code> are OK, however, <code class="docutils literal notranslate"><span class="pre">Just</span> <span class="pre">(Just</span> <span class="pre">a)</span></code>
 will be rejected.  This is a restriction that we may lift in the future.</p>
+<p><strong>No Overlapping Patterns.</strong> For simplicity, all patterns in a
+<code class="docutils literal notranslate"><span class="pre">case</span></code> expression must be disjoint. In particular, this means that:</p>
+<blockquote>
+<div><ul>
+<li><p>No two patterns in a <code class="docutils literal notranslate"><span class="pre">case</span></code> expression can match the same constructor.
+This means that Cryptol will reject the following example:</p>
+<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">isNothing</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span>
+<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">of</span>
+<span class="w">    </span><span class="kt">Nothing</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">True</span>
+<span class="w">    </span><span class="kt">Nothing</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">False</span>
+</pre></div>
+</div>
+</li>
+<li><p>If a <code class="docutils literal notranslate"><span class="pre">case</span></code> expression uses a catch-all clause, then that clause must
+occur last in the expression. It is an error to match on additional
+patterns after the catch-all clause. For instance, Cryptol will reject the
+following example:</p>
+<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">isNothing</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span>
+<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">of</span>
+<span class="w">    </span><span class="kt">Just</span><span class="w"> </span><span class="n">_</span><span class="w">  </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">False</span>
+<span class="w">    </span><span class="n">_</span><span class="w">       </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">True</span>
+<span class="w">    </span><span class="kt">Nothing</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">False</span>
+</pre></div>
+</div>
+</li>
+</ul>
+</div></blockquote>
+<p><strong>Patterns Must Be Exhaustive.</strong> The patterns in a <code class="docutils literal notranslate"><span class="pre">case</span></code> expression must
+cover all constructors in the <code class="docutils literal notranslate"><span class="pre">enum</span></code> type being matched on. For example,
+Cryptol will reject the following example, as it does not cover the <code class="docutils literal notranslate"><span class="pre">Just</span></code>
+constructor:</p>
+<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">isNothing</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span>
+<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">of</span>
+<span class="w">    </span><span class="kt">Nothing</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">True</span>
+</pre></div>
+</div>
+<p><strong>The Matched Expression Must Have a Knwon Enum Type.</strong> Cryptol will reject
+the definition of <code class="docutils literal notranslate"><span class="pre">f</span></code>, where <code class="docutils literal notranslate"><span class="pre">f</span></code> lacks a type signature, or is not not
+an <code class="docutils literal notranslate"><span class="pre">enum</span></code> type.</p>
+<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span>
+<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">of</span>
+<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="nb">()</span>
+</pre></div>
+</div>
+<p>This is because it is not clear what the type of <code class="docutils literal notranslate"><span class="pre">x</span></code> (the expression being
+matched) should be. The only pattern is a catch-all case, which does not reveal
+anything about the type of <code class="docutils literal notranslate"><span class="pre">x</span></code>. It would be incorrect to give <code class="docutils literal notranslate"><span class="pre">f</span></code> this type:</p>
+<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="nb">()</span>
+</pre></div>
+</div>
+<p>This is because <code class="docutils literal notranslate"><span class="pre">f</span></code> is not really polymorphic in its argument type, as the
+only values that can be matched in a <code class="docutils literal notranslate"><span class="pre">case</span></code> expression are those whose type
+was declared as an <code class="docutils literal notranslate"><span class="pre">enum</span></code>. As such, Cryptol rejects this example.</p>
 </section>
 </section>
 

docs/RefMan/_build/html/_sources/TypeDeclarations.rst.txt

@@ -51,18 +51,19 @@ of newtypes to extract the values in the body of the type.
   > sum x.seq
   6
 
-Enumerations
-------------
+Enums
+-----
 
 .. code-block:: cryptol
 
   enum Maybe a = Nothing | Just a
 
-An ``enum`` declaration introduces a new named type, which is defined by
-a collection of *constructors*.  Each named ``enum`` type is treated like
-a separate type, even if it has the exact same constructors as another ``enum``
-type---in this way ``enum`` is similar to ``newtype`` and unlike ``type``
-synonyms.
+An ``enum`` declaration introduces a new named type, which is defined by a
+collection of *constructors*. ``enum`` declarations correspond to the notion of
+*algebraic data types*, which are commonly found in other programming
+languages. Each named ``enum`` type is treated like a separate type, even if it
+has the exact same constructors as another ``enum`` type---in this way ``enum``
+is similar to ``newtype`` and unlike ``type`` synonyms.
 
 **Constructors.** The only way to create a value of an ``enum`` type is to
 use one of its constructors.   When used in an expression, the constructors
@@ -120,17 +121,66 @@ as long as this type does not depend on the type to which the constructor
 belongs.  This means that we do not support defining recursive types,
 such as linked lists.
 
-**No Nested Consturctor Patterns.**  For simplicity, only non-constructor
+**No Nested Constructor Patterns.**  For simplicity, only non-constructor
 patterns may be used in the fields of a constructor pattern.  For example,
 ``Just (a,b)`` and ``Just (a # b)`` are OK, however, ``Just (Just a)``
 will be rejected.  This is a restriction that we may lift in the future.
 
+**No Overlapping Patterns.** For simplicity, all patterns in a
+``case`` expression must be disjoint. In particular, this means that:
 
+  * No two patterns in a ``case`` expression can match the same constructor.
+    This means that Cryptol will reject the following example:
 
+    .. code-block:: cryptol
 
+      isNothing x =
+        case x of
+          Nothing -> True
+          Nothing -> False
 
+  * If a ``case`` expression uses a catch-all clause, then that clause must
+    occur last in the expression. It is an error to match on additional
+    patterns after the catch-all clause. For instance, Cryptol will reject the
+    following example:
 
+    .. code-block:: cryptol
 
+      isNothing x =
+        case x of
+          Just _  -> False
+          _       -> True
+          Nothing -> False
 
+**Patterns Must Be Exhaustive.** The patterns in a ``case`` expression must
+cover all constructors in the ``enum`` type being matched on. For example,
+Cryptol will reject the following example, as it does not cover the ``Just``
+constructor:
 
+.. code-block:: cryptol
+
+  isNothing x =
+    case x of
+      Nothing -> True
+
+**The Matched Expression Must Have a Knwon Enum Type.** Cryptol will reject
+the definition of ``f``, where ``f`` lacks a type signature, or is not not
+an ``enum`` type.
+
+.. code-block:: cryptol
+
+  f x =
+    case x of
+      _ -> ()
+
+This is because it is not clear what the type of ``x`` (the expression being
+matched) should be. The only pattern is a catch-all case, which does not reveal
+anything about the type of ``x``. It would be incorrect to give ``f`` this type:
+
+.. code-block:: cryptol
+
+  f : {a} a -> ()
 
+This is because ``f`` is not really polymorphic in its argument type, as the
+only values that can be matched in a ``case`` expression are those whose type
+was declared as an ``enum``. As such, Cryptol rejects this example.

src/Cryptol/TypeCheck/Error.hs

@@ -94,10 +94,10 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
               | TypeMismatch TypeSource Path Type Type
                 -- ^ Expected type, inferred type
 
-              | EnumTypeMismatch TypeSource Path Type
+              | EnumTypeMismatch Type
                 -- ^ Expected an enum type, but inferred the supplied 'Type'
-                --   instead, which is too ambiguous. This corresponds to the
-                --   \"Matched Expression Must Have an Unambiguous Type\"
+                --   instead, which is no an enum. This corresponds to the
+                --   \"Matched Expression Must Have a Known Enum Type\"
                 --   restriction for @case@ expressions, as described in the
                 --   Cryptol Reference Manual.
 
@@ -304,7 +304,7 @@ instance TVars Error where
       SchemaMismatch i t1 t2  ->
         SchemaMismatch i !$ (apSubst su t1) !$ (apSubst su t2)
       TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)
-      EnumTypeMismatch src pa t -> EnumTypeMismatch src pa !$ apSubst su t
+      EnumTypeMismatch t        -> EnumTypeMismatch !$ apSubst su t
       InvalidConPat {}          -> err
       UncoveredConPat {}        -> err
       OverlappingPat {}         -> err
@@ -358,7 +358,7 @@ instance FVS Error where
       RecursiveTypeDecls {}     -> Set.empty
       SchemaMismatch _ t1 t2    -> fvs (t1,t2)
       TypeMismatch _ _ t1 t2    -> fvs (t1,t2)
-      EnumTypeMismatch _ _ t    -> fvs t
+      EnumTypeMismatch t        -> fvs t
       InvalidConPat {}          -> Set.empty
       UncoveredConPat {}        -> Set.empty
       OverlappingPat {}         -> Set.empty
@@ -492,16 +492,18 @@ instance PP (WithNames Error) where
             ++ ppCtxt pa
             ++ ["When checking" <+> pp src]
 
-      EnumTypeMismatch src pa t ->
-        addTVarsDescsAfter names err $
-        nested "Type mismatch:" $
-        vcat $
-          [ "Expected an enum type, but"
-          , "the inferred type" <+> parens (ppWithNames names t) <+>
-            "is ambiguous."
-          , "Try giving the expression an explicit type."
-          ] ++ ppCtxt pa
-            ++ ["When checking" <+> pp src]
+      EnumTypeMismatch t ->
+        case tNoUser t of
+          TVar {} ->
+            nested "Failed to infer the type of cased expression."
+              "Try giving the expression an explicit type annotation."
+          _ ->
+            addTVarsDescsAfter names err $
+            nested "Type mismatch in cased expresson:" $
+              vcat
+                [ "Expected: an `enum` type"
+                , "Inferred:" <+> ppWithNames names t
+                ]
 
       SchemaMismatch i t1 t2 ->
           addTVarsDescsAfter names err $

src/Cryptol/TypeCheck/Infer.hs

@@ -523,12 +523,9 @@ checkE expr tGoal =
 
         -- Check that the type of the scrutinee is unambiguously an enum.
         et' <- applySubst et
-        let expect = WithSource
-                       { twsType = et'
-                       , twsRange = Just rng
-                       , twsSource = CasedExpression
-                       }
-        cons <- expectEnum expect
+        cons <- case getLoc e of
+                 Just r -> inRange r (expectEnum et')
+                 Nothing -> expectEnum et'
 
         -- Check that the case expression covers all possible constructors.
         -- If there is a default case, there is no need to check anything,
@@ -740,18 +737,18 @@ expectRec fs tGoal@(WithSource ty src rng) =
 
 -- | Retrieve the constructors from a type that is expected to be unambiguously
 -- an enum, throwing an error if this is not the case.
-expectEnum :: TypeWithSource -> InferM [EnumCon]
-expectEnum (WithSource ty src rng) =
+expectEnum :: Type -> InferM [EnumCon]
+expectEnum ty =
   case ty of
     TUser _ _ ty' ->
-      expectEnum (WithSource ty' src rng)
+      expectEnum ty'
 
     TNominal nt _
       |  Enum ecs <- ntDef nt
       -> pure ecs
 
     _ -> do
-      recordErrorLoc rng (EnumTypeMismatch src rootPath ty)
+      recordError (EnumTypeMismatch ty)
       pure []
 
 expectFin :: Int -> TypeWithSource -> InferM ()

tests/enum/CaseAmbiguousType.cry

@@ -1,3 +1,7 @@
 f e =
   case e of
     _ -> ()
+
+g e =
+  case e : Integer of
+    _ -> ()

tests/enum/CaseAmbiguousType.icry.stdout

@@ -2,11 +2,10 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 
-[error] at CaseAmbiguousType.cry:2:3--5:0:
-  Type mismatch:
-    Expected an enum type, but
-    the inferred type (?a) is ambiguous.
-    Try giving the expression an explicit type.
-    When checking cased expression
-  where
-  ?a is the type of 'e' at CaseAmbiguousType.cry:1:3--1:4
+[error] at CaseAmbiguousType.cry:2:8--2:9:
+  Failed to infer the type of cased expression.
+    Try giving the expression an explicit type annotation.
+[error] at CaseAmbiguousType.cry:6:8--6:19:
+  Type mismatch in cased expresson:
+    Expected: an `enum` type
+    Inferred: Integer