Make a friendlier, non-panic error message for cases where patterns

introduce nontrivial constraints.

Fixes #290

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

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. -}

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 =

tests/issues/issue290v2.cry

@@ -0,0 +1,2 @@
+minMax : {n, a} (fin n, Cmp a) => [n]a -> (a,a)
+minMax [x] = (x,x)

tests/issues/issue290v2.icry

@@ -0,0 +1 @@
+:load issue290v2.cry

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