From b6a83d7cb802d0ad39ef55ed7804f25c428a59c2 Mon Sep 17 00:00:00 2001
From: Robert Dockins <rdockins@galois.com>
Date: Wed, 4 May 2016 17:38:16 -0700
Subject: [PATCH] Make a friendlier, non-panic error message for cases where
 patterns introduce nontrivial constraints.

Fixes #290
---
 src/Cryptol/Parser/AST.hs           |  2 ++
 src/Cryptol/TypeCheck/Infer.hs      | 12 +++++-------
 src/Cryptol/TypeCheck/InferTypes.hs |  3 +++
 tests/issues/issue290v2.cry         |  2 ++
 tests/issues/issue290v2.icry        |  1 +
 tests/issues/issue290v2.icry.stdout | 10 ++++++++++
 6 files changed, 23 insertions(+), 7 deletions(-)
 create mode 100644 tests/issues/issue290v2.cry
 create mode 100644 tests/issues/issue290v2.icry
 create mode 100644 tests/issues/issue290v2.icry.stdout

diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs
index 735bdb5e..95c106ae 100644
--- a/src/Cryptol/Parser/AST.hs
+++ b/src/Cryptol/Parser/AST.hs
@@ -473,6 +473,8 @@ instance AddLoc (Pattern name) where
 
 instance HasLoc (Pattern name) where
   getLoc (PLocated _ r) = Just r
+  getLoc (PTyped r _)   = getLoc r
+  getLoc (PVar x)       = getLoc x
   getLoc _              = Nothing
 
 instance HasLoc (Bind name) where
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index 98eb5e29..3481e67f 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -36,14 +36,12 @@ import qualified Data.Map as Map
 import           Data.Map (Map)
 import qualified Data.Set as Set
 import           Data.Either(partitionEithers)
-import           Data.Maybe(mapMaybe,isJust)
+import           Data.Maybe(mapMaybe,isJust, fromMaybe)
 import           Data.List(partition,find)
 import           Data.Graph(SCC(..))
 import           Data.Traversable(forM)
 import           Control.Monad(when,zipWithM)
 
--- import Cryptol.Utils.Debug
-
 inferModule :: P.Module Name -> InferM Module
 inferModule m =
   inferDs (P.mDecls m) $ \ds1 ->
@@ -491,14 +489,14 @@ smallest ts   = do a <- newType (text "length of list comprehension") KNum
                    newGoals CtComprehension [ a =#= foldr1 tMin ts ]
                    return a
 
-
 checkP :: Doc -> P.Pattern Name -> Type -> InferM (Located Name)
 checkP desc p tGoal =
   do (x, t) <- inferP desc p
      ps <- unify tGoal (thing t)
-     case ps of
-       [] -> return (Located (srcRange t) x)
-       _  -> tcPanic "checkP" [ "Unexpected constraints:", show ps ]
+     let rng   = fromMaybe emptyRange $ getLoc p
+     let mkErr = recordError . UnsolvedGoal False . Goal (CtPattern desc) rng
+     mapM_ mkErr ps
+     return (Located (srcRange t) x)
 
 {-| Infer the type of a pattern.  Assumes that the pattern will be just
 a variable. -}
diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs
index 69ac6708..82d8af32 100644
--- a/src/Cryptol/TypeCheck/InferTypes.hs
+++ b/src/Cryptol/TypeCheck/InferTypes.hs
@@ -190,6 +190,7 @@ data ConstraintSource
   | CtDefaulting          -- ^ Just defaulting on the command line
   | CtPartialTypeFun TyFunName -- ^ Use of a partial type function.
   | CtImprovement
+  | CtPattern Doc         -- ^ Constraints arising from type-checking patterns
     deriving (Show,Generic)
 
 instance NFData ConstraintSource where rnf = genericRnf
@@ -216,6 +217,7 @@ instance TVars ConstraintSource where
       CtDefaulting    -> src
       CtPartialTypeFun _ -> src
       CtImprovement    -> src
+      CtPattern _      -> src
 
 instance TVars Warning where
   apSubst su warn =
@@ -519,6 +521,7 @@ instance PP ConstraintSource where
       CtDefaulting    -> text "defaulting"
       CtPartialTypeFun f -> text "use of partial type function" <+> pp f
       CtImprovement   -> text "examination of collected goals"
+      CtPattern desc  -> text "checking a pattern:" <+> desc
 
 ppUse :: Expr -> Doc
 ppUse expr =
diff --git a/tests/issues/issue290v2.cry b/tests/issues/issue290v2.cry
new file mode 100644
index 00000000..22f34a02
--- /dev/null
+++ b/tests/issues/issue290v2.cry
@@ -0,0 +1,2 @@
+minMax : {n, a} (fin n, Cmp a) => [n]a -> (a,a)
+minMax [x] = (x,x)
diff --git a/tests/issues/issue290v2.icry b/tests/issues/issue290v2.icry
new file mode 100644
index 00000000..50968b25
--- /dev/null
+++ b/tests/issues/issue290v2.icry
@@ -0,0 +1 @@
+:load issue290v2.cry
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
new file mode 100644
index 00000000..56052d3b
--- /dev/null
+++ b/tests/issues/issue290v2.icry.stdout
@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at ./issue290v2.cry:2:1--2:19:
+  Unsolved constraint:
+    a`195 == 1
+      arising from
+      checking a pattern: type of 1st argument of Main::minMax
+      at ./issue290v2.cry:2:8--2:11