Improve error reporting for untouchable type variables
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 8 Apr 2014 16:37:45 +0000 (17:37 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 8 Apr 2014 16:37:59 +0000 (17:37 +0100)
This change adds a suggestion
    Possible fix: add a type signature for ‘f’
when we have a GADT-style definition with a
type we can't figure out.

See Note [Suggest adding a type signature] in TcErrors.

This initially came up in the discussion of Trac #8968.

compiler/typecheck/TcErrors.lhs
testsuite/tests/gadt/gadt-escape1.stderr
testsuite/tests/gadt/gadt13.stderr
testsuite/tests/gadt/gadt7.stderr
testsuite/tests/polykinds/T7438.stderr
testsuite/tests/polykinds/T7594.stderr

index df241c9..629c7a8 100644 (file)
@@ -48,7 +48,7 @@ import DynFlags
 import ListSetOps       ( equivClasses )
 
 import Data.Maybe
-import Data.List        ( partition, mapAccumL, zip4 )
+import Data.List        ( partition, mapAccumL, zip4, nub )
 \end{code}
 
 %************************************************************************
@@ -728,14 +728,15 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
   = do { let msg = misMatchMsg oriented ty1 ty2
-             untch_extra 
+             untch_extra
                 = nest 2 $
                   sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable")
                       , nest 2 $ ptext (sLit "inside the constraints") <+> pprEvVarTheta given
                       , nest 2 $ ptext (sLit "bound by") <+> ppr skol_info
                       , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ]
              tv_extra = extraTyVarInfo ctxt ty1 ty2
-       ; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, extra]) }
+             add_sig  = suggestAddSig ctxt ty1 ty2
+       ; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, add_sig, extra]) }
 
   | otherwise
   = reportEqErr ctxt extra ct oriented (mkTyVarTy tv1) ty2
@@ -815,29 +816,42 @@ pp_givens givens
                        , ptext (sLit "at") <+> ppr loc])
 
 extraTyVarInfo :: ReportErrCtxt -> TcType -> TcType -> SDoc
--- Add on extra info about the types themselves
+-- Add on extra info about skolem constants
 -- NB: The types themselves are already tidied
 extraTyVarInfo ctxt ty1 ty2
-  = nest 2 (extra1 $$ extra2)
+  = nest 2 (tv_extra ty1 $$ tv_extra ty2)
   where
-    extra1 = tyVarExtraInfoMsg (cec_encl ctxt) ty1
-    extra2 = tyVarExtraInfoMsg (cec_encl ctxt) ty2
-
-tyVarExtraInfoMsg :: [Implication] -> Type -> SDoc
--- Shows a bit of extra info about skolem constants
-tyVarExtraInfoMsg implics ty
-  | Just tv <- tcGetTyVar_maybe ty
-  , isTcTyVar tv, isSkolemTyVar tv
-  , let pp_tv = quotes (ppr tv)
- = case tcTyVarDetails tv of
-    SkolemTv {}   -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
-    FlatSkol {}   -> pp_tv <+> ptext (sLit "is a flattening type variable")
-    RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
-    MetaTv {}     -> empty
-
- | otherwise             -- Normal case
- = empty
+    implics = cec_encl ctxt
+    tv_extra ty | Just tv <- tcGetTyVar_maybe ty
+                , isTcTyVar tv, isSkolemTyVar tv
+                , let pp_tv = quotes (ppr tv)
+                = case tcTyVarDetails tv of
+                    SkolemTv {}   -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
+                    FlatSkol {}   -> pp_tv <+> ptext (sLit "is a flattening type variable")
+                    RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
+                    MetaTv {}     -> empty
+
+                | otherwise             -- Normal case
+                = empty
+
+suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
+-- See Note [Suggest adding a type signature]
+suggestAddSig ctxt ty1 ty2
+  | null inferred_bndrs
+  = empty
+  | [bndr] <- inferred_bndrs
+  = ptext (sLit "Possible fix: add a type signature for") <+> quotes (ppr bndr)
+  | otherwise
+  = ptext (sLit "Possible fix: add type signatures for some or all of") <+> (ppr inferred_bndrs)
+  where
+    inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
+    get_inf ty | Just tv <- tcGetTyVar_maybe ty
+               , isTcTyVar tv, isSkolemTyVar tv
+               , InferSkol prs <- getSkolemInfo (cec_encl ctxt) tv
+               = map fst prs
+               | otherwise
+               = []
+
 kindErrorMsg :: TcType -> TcType -> SDoc   -- Types are already tidy
 kindErrorMsg ty1 ty2
   = vcat [ ptext (sLit "Kind incompatibility when matching types:")
@@ -907,6 +921,23 @@ sameOccExtra ty1 ty2
          loc = nameSrcSpan nm
 \end{code}
 
+Note [Suggest adding a type signature]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The OutsideIn algorithm rejects GADT programs that don't have a principal
+type, and indeed some that do.  Example:
+   data T a where
+     MkT :: Int -> T Int
+
+   f (MkT n) = n
+
+Does this have type f :: T a -> a, or f :: T a -> Int?
+The error that shows up tends to be an attempt to unify an
+untouchable type variable.  So suggestAddSig sees if the offending
+type variable is bound by an *inferred* signature, and suggests
+adding a declared signature instead.
+
+This initially came up in Trac #8968, concerning pattern synonyms.
+
 Note [Disambiguating (X ~ X) errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See Trac #8278
index 1ec5ea8..35d1bf4 100644 (file)
@@ -9,6 +9,7 @@ gadt-escape1.hs:19:58:
         at gadt-escape1.hs:19:43-50
       ‘t’ is a rigid type variable bound by
           the inferred type of weird1 :: t at gadt-escape1.hs:19:1
+    Possible fix: add a type signature for ‘weird1’
     Expected type: t
       Actual type: ExpGADT t1
     Relevant bindings include
index 5861424..563492d 100644 (file)
@@ -10,6 +10,7 @@ gadt13.hs:15:13:
         at gadt13.hs:15:6-8
       ‘t’ is a rigid type variable bound by
           the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
+    Possible fix: add a type signature for ‘shw’
     Relevant bindings include
       shw :: Term t1 -> t (bound at gadt13.hs:15:1)
     In the expression: ("I " ++) . shows t
index 4ce8ad4..3fb4a6a 100644 (file)
@@ -11,6 +11,7 @@ gadt7.hs:16:38:
            the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
       ‘t’ is a rigid type variable bound by
           the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
+    Possible fix: add a type signature for ‘i1b’
     Relevant bindings include
       y1 :: t1 (bound at gadt7.hs:16:16)
       y :: t1 (bound at gadt7.hs:16:7)
index 92e01e7..b126621 100644 (file)
@@ -1,18 +1,19 @@
-\r
-T7438.hs:6:14:\r
-    Couldn't match expected type ‘t1’ with actual type ‘t’\r
-      ‘t’ is untouchable\r
-        inside the constraints (t2 ~ t3)\r
-        bound by a pattern with constructor\r
-                   Nil :: forall (a :: k). Thrist a a,\r
-                 in an equation for ‘go’\r
-        at T7438.hs:6:4-6\r
-      ‘t’ is a rigid type variable bound by\r
-          the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1\r
-      ‘t1’ is a rigid type variable bound by\r
-           the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1\r
-    Relevant bindings include\r
-      acc :: t (bound at T7438.hs:6:8)\r
-      go :: Thrist t2 t3 -> t -> t1 (bound at T7438.hs:6:1)\r
-    In the expression: acc\r
-    In an equation for ‘go’: go Nil acc = acc\r
+
+T7438.hs:6:14:
+    Couldn't match expected type ‘t1’ with actual type ‘t’
+      ‘t’ is untouchable
+        inside the constraints (t2 ~ t3)
+        bound by a pattern with constructor
+                   Nil :: forall (a :: k). Thrist a a,
+                 in an equation for ‘go’
+        at T7438.hs:6:4-6
+      ‘t’ is a rigid type variable bound by
+          the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
+      ‘t1’ is a rigid type variable bound by
+           the inferred type of go :: Thrist t2 t3 -> t -> t1 at T7438.hs:6:1
+    Possible fix: add a type signature for ‘go’
+    Relevant bindings include
+      acc :: t (bound at T7438.hs:6:8)
+      go :: Thrist t2 t3 -> t -> t1 (bound at T7438.hs:6:1)
+    In the expression: acc
+    In an equation for ‘go’: go Nil acc = acc
index a01b24d..31faf3d 100644 (file)
@@ -7,6 +7,7 @@ T7594.hs:33:12:
         at T7594.hs:33:8-19
       ‘b’ is a rigid type variable bound by
           the inferred type of bar2 :: b at T7594.hs:33:1
+    Possible fix: add a type signature for ‘bar2’
     Expected type: a -> b
       Actual type: a -> IO ()
     Relevant bindings include bar2 :: b (bound at T7594.hs:33:1)