Improve error reporting for kind errors (fix Trac #1633)

[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index ecee5ac..e5e16fc 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -14,7 +14,6 @@ module TcUnify (
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,

-  checkExpectedKind,

   preSubType, boxyMatchTypes,
 
   --------------------------------
   preSubType, boxyMatchTypes,
 
   --------------------------------

@@ -79,7 +78,9 @@ tcInfer tc_infer = withBox openTypeKind tc_infer
 subFunTys :: SDoc  -- Something like "The function f has 3 arguments"
                    -- or "The abstraction (\x.e) takes 1 argument"
           -> Arity              -- Expected # of args
 subFunTys :: SDoc  -- Something like "The function f has 3 arguments"
                    -- or "The abstraction (\x.e) takes 1 argument"
           -> Arity              -- Expected # of args

-          -> BoxyRhoType        -- res_ty
+          -> BoxySigmaType      -- res_ty
+         -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature
+                               -- Only relevant if we encounter a sigma-type

           -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
           -> TcM (HsWrapper, a)
 -- Attempt to decompse res_ty to have enough top-level arrows to
           -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
           -> TcM (HsWrapper, a)
 -- Attempt to decompse res_ty to have enough top-level arrows to

@@ -108,7 +109,7 @@ subFunTys :: SDoc  -- Something like "The function f has 3 arguments"
 -}
 
 
 -}
 
 

-subFunTys error_herald n_pats res_ty thing_inside
+subFunTys error_herald n_pats res_ty mb_ctxt thing_inside

   = loop n_pats [] res_ty
   where
         -- In 'loop', the parameter 'arg_tys' accumulates
   = loop n_pats [] res_ty
   where
         -- In 'loop', the parameter 'arg_tys' accumulates

@@ -121,8 +122,8 @@ subFunTys error_herald n_pats res_ty thing_inside
         | isSigmaTy res_ty      -- Do this before checking n==0, because we
                                 -- guarantee to return a BoxyRhoType, not a
                                 -- BoxySigmaType
         | isSigmaTy res_ty      -- Do this before checking n==0, because we
                                 -- guarantee to return a BoxyRhoType, not a
                                 -- BoxySigmaType

-        = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
-                                         loop n args_so_far res_ty'
+        = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty ->
+                                         loop n args_so_far res_ty

              ; return (gen_fn <.> co_fn, res) }
 
     loop 0 args_so_far res_ty
              ; return (gen_fn <.> co_fn, res) }
 
     loop 0 args_so_far res_ty

@@ -609,7 +610,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 

-    go _ (TyVarTy tv) | isMetaTyVar tv
+    go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+                               -- NB: A TyVar (not TcTyVar) is possible here, representing
+                               --     a skolem, because in this pure boxy_match function 
+                               --     we don't instantiate foralls to TcTyVars; cf Trac #2714

         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable
         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable

@@ -768,7 +772,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
     if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
         defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
     else do
     if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
         defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
     else do

-        { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
+        { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty ->

                              tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
         ; return (gen_fn <.> co_fn) }
     }
                              tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
         ; return (gen_fn <.> co_fn) }
     }

@@ -894,26 +898,21 @@ wrapFunResCoercion arg_tys co_fn_res
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-tcGen :: BoxySigmaType                          -- expected_ty
-      -> TcTyVarSet                             -- Extra tyvars that the universally
-                                                --      quantified tyvars of expected_ty
-                                                --      must not be unified
+tcGen :: BoxySigmaType                -- expected_ty
+      -> TcTyVarSet                   -- Extra tyvars that the universally
+                                      --      quantified tyvars of expected_ty
+                                      --      must not be unified
+      -> Maybe UserTypeCtxt          -- Just ctxt => this polytype arose directly
+                                     --                from a user type sig
+                                     -- Nothing => a higher order situation

       -> ([TcTyVar] -> BoxyRhoType -> TcM result)
       -> TcM (HsWrapper, result)
         -- The expression has type: spec_ty -> expected_ty
 
       -> ([TcTyVar] -> BoxyRhoType -> TcM result)
       -> TcM (HsWrapper, result)
         -- The expression has type: spec_ty -> expected_ty
 

-tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
-                                                -- If not, the call is a no-op
+tcGen expected_ty extra_tvs mb_ctxt thing_inside        -- We expect expected_ty to be a forall-type
+                                                       -- If not, the call is a no-op

   = do  { traceTc (text "tcGen")
   = do  { traceTc (text "tcGen")

-                -- We want the GenSkol info in the skolemised type variables to
-                -- mention the *instantiated* tyvar names, so that we get a
-                -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
-                -- Hence the tiresome but innocuous fixM
-        ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
-                do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
-                        -- Get loation from monad, not from expected_ty
-                   ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
-                   ; return ((forall_tvs, theta, rho_ty), skol_info) })
+        ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty

 
         ; when debugIsOn $
               traceTc (text "tcGen" <+> vcat [
 
         ; when debugIsOn $
               traceTc (text "tcGen" <+> vcat [

@@ -924,7 +923,8 @@ tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a
                            text "free_tvs" <+> ppr free_tvs])
 
         -- Type-check the arg and unify with poly type
                            text "free_tvs" <+> ppr free_tvs])
 
         -- Type-check the arg and unify with poly type

-        ; (result, lie) <- getLIE (thing_inside tvs' rho')
+        ; (result, lie) <- getLIE $ 
+                          thing_inside tvs' rho'

 
         -- Check that the "forall_tvs" havn't been constrained
         -- The interesting bit here is that we must include the free variables
 
         -- Check that the "forall_tvs" havn't been constrained
         -- The interesting bit here is that we must include the free variables

@@ -951,6 +951,23 @@ tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a
         ; return (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
         ; return (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs

+
+    instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo)
+    instantiate expected_ty
+      | Just ctxt <- mb_ctxt   -- This case split is the wohle reason for mb_ctxt
+      = do { let skol_info = SigSkol ctxt
+           ; stuff <- tcInstSigType True skol_info expected_ty
+          ; return (stuff, skol_info) }
+
+      | otherwise   -- We want the GenSkol info in the skolemised type variables to
+                    -- mention the *instantiated* tyvar names, so that we get a
+                   -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+                   -- Hence the tiresome but innocuous fixM
+      = fixM $ \ ~(_, skol_info) ->
+        do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
+                -- Get loation from *monad*, not from expected_ty
+           ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
+           ; return (stuff, skol_info) }

 \end{code}
 
 
 \end{code}
 
 

@@ -1177,13 +1194,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
     go outer _ (PredTy p1) _ (PredTy p2)
         = uPred outer nb1 p1 nb2 p2
 
     go outer _ (PredTy p1) _ (PredTy p2)
         = uPred outer nb1 p1 nb2 p2
 

-        -- Type constructors must match
+        -- Non-synonym type constructors must match

     go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
       = do { cois <- uTys_s nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }
     go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
       = do { cois <- uTys_s nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }

-        -- See Note [TyCon app]
+        -- Family synonyms See Note [TyCon app]

       | con1 == con2 && identicalOpenSynTyConApp
       = do { cois <- uTys_s nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
       | con1 == con2 && identicalOpenSynTyConApp
       = do { cois <- uTys_s nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)

@@ -1195,6 +1212,29 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
         -- See Note [OpenSynTyCon app]
 
         identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
         -- See Note [OpenSynTyCon app]
 

+        -- If we can reduce a family app => proceed with reduct
+        -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+        --     defer oversaturated applications!
+    go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
+      | isOpenSynTyCon con1
+      = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+           ; case coi1 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
+           }
+
+        -- If we can reduce a family app => proceed with reduct
+        -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+        --     defer oversaturated applications!
+    go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
+      | isOpenSynTyCon con2
+      = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+           ; case coi2 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (`mkTransCoI` mkSymCoI coi2) $ 
+                         go outer sty1 ty1 sty2 ty2'
+           }
+

         -- Functions; just check the two parts
     go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
       = do { coi_l <- uTys nb1 fun1 nb2 fun2
         -- Functions; just check the two parts
     go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
       = do { coi_l <- uTys nb1 fun1 nb2 fun2

@@ -1220,36 +1260,12 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
            ; coi_t <- uTys nb1 t1 nb2 t2
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 
            ; coi_t <- uTys nb1 t1 nb2 t2
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 

-        -- One or both outermost constructors are type family applications.
-        -- If we can normalise them away, proceed as usual; otherwise, we
-        -- need to defer unification by generating a wanted equality constraint.
-    go outer sty1 ty1 sty2 ty2
-      | ty1_is_fun || ty2_is_fun
-      = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
-                                           else return (IdCo, ty1)
-           ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
-                                           else return (IdCo, ty2)
-           ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
-                    then do { -- One type family app can't be reduced yet
-                              -- => defer
-                            ; ty1'' <- zonkTcType ty1'
-                            ; ty2'' <- zonkTcType ty2'
-                            ; if tcEqType ty1'' ty2''
-                              then return IdCo
-                              else -- see [Deferred Unification]
-                                defer_unification outer False orig_ty1 orig_ty2
-                            }
-                     else -- unification can proceed
-                          go outer sty1 ty1' sty2 ty2'
-           ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
-           }
-        where
-          ty1_is_fun = isOpenSynTyConApp ty1
-          ty2_is_fun = isOpenSynTyConApp ty2
-

         -- Anything else fails
     go outer _ _ _ _ = bale_out outer
 
         -- Anything else fails
     go outer _ _ _ _ = bale_out outer
 

+    defer = defer_unification outer False orig_ty1 orig_ty2
+
+

 ----------
 uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
 uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
 ----------
 uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
 uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)

@@ -1280,8 +1296,8 @@ Note [TyCon app]
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two

-AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2).  In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app).  If we unify f1~f2 first,

 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 
 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 

@@ -1856,7 +1872,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *

--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *

 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where

@@ -1904,75 +1920,6 @@ unifyFunKind _                         = return Nothing
 
 %************************************************************************
 %*                                                                      *
 
 %************************************************************************
 %*                                                                      *

-        Checking kinds
-%*                                                                      *
-%************************************************************************
-
----------------------------
--- We would like to get a decent error message from
---   (a) Under-applied type constructors
---              f :: (Maybe, Maybe)
---   (b) Over-applied type constructors
---              f :: Int x -> Int x
---
-
-\begin{code}
-checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
--- A fancy wrapper for 'unifyKind', which tries
--- to give decent error messages.
---      (checkExpectedKind ty act_kind exp_kind)
--- checks that the actual kind act_kind is compatible
---      with the expected kind exp_kind
--- The first argument, ty, is used only in the error message generation
-checkExpectedKind ty act_kind exp_kind
-  | act_kind `isSubKind` exp_kind -- Short cut for a very common case
-  = return ()
-  | otherwise = do
-    (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
-    case mb_r of
-        Just _  -> return ()  -- Unification succeeded
-        Nothing -> do
-
-        -- So there's definitely an error
-        -- Now to find out what sort
-           exp_kind <- zonkTcKind exp_kind
-           act_kind <- zonkTcKind act_kind
-
-           env0 <- tcInitTidyEnv
-           let (exp_as, _) = splitKindFunTys exp_kind
-               (act_as, _) = splitKindFunTys act_kind
-               n_exp_as = length exp_as
-               n_act_as = length act_as
-
-               (env1, tidy_exp_kind) = tidyKind env0 exp_kind
-               (env2, tidy_act_kind) = tidyKind env1 act_kind
-
-               err | n_exp_as < n_act_as     -- E.g. [Maybe]
-                   = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
-
-                     -- Now n_exp_as >= n_act_as. In the next two cases,
-                     -- n_exp_as == 0, and hence so is n_act_as
-                   | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
-                   = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is unlifted")
-
-                   | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
-                   = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is lifted")
-
-                   | otherwise               -- E.g. Monad [Int]
-                   = ptext (sLit "Kind mis-match")
-
-               more_info = sep [ ptext (sLit "Expected kind") <+>
-                                     quotes (pprKind tidy_exp_kind) <> comma,
-                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
-                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
-           failWithTcM (env2, err $$ more_info)
-\end{code}
-
-%************************************************************************
-%*                                                                      *

 \subsection{Checking signature type variables}
 %*                                                                      *
 %************************************************************************
 \subsection{Checking signature type variables}
 %*                                                                      *
 %************************************************************************

@@ -2024,7 +1971,7 @@ check_sig_tyvars
 check_sig_tyvars _ []
   = return ()
 check_sig_tyvars extra_tvs sig_tvs
 check_sig_tyvars _ []
   = return ()
 check_sig_tyvars extra_tvs sig_tvs

-  = ASSERT( all isSkolemTyVar sig_tvs )
+  = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )

     do  { gbl_tvs <- tcGetGlobalTyVars
         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                       text "gbl_tvs" <+> ppr gbl_tvs,
     do  { gbl_tvs <- tcGetGlobalTyVars
         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                       text "gbl_tvs" <+> ppr gbl_tvs,