Fix #14916 with an additional validity check in deriveTyData
[ghc.git] / compiler / typecheck / TcValidity.hs
index d8e2519..d2d32c6 100644 (file)
@@ -9,7 +9,7 @@ module TcValidity (
   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
   ContextKind(..), expectedKindInCtxt,
   checkValidTheta, checkValidFamPats,
-  checkValidInstance, validDerivPred,
+  checkValidInstance, checkValidInstHead, validDerivPred,
   checkInstTermination, checkTySynRhs,
   ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn,
@@ -20,6 +20,8 @@ module TcValidity (
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Maybes
 
 -- friends:
@@ -39,7 +41,7 @@ import TyCon
 -- others:
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
-import TcEnv       ( tcGetInstEnvs )
+import TcEnv       ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv )
 import FunDeps
 import InstEnv     ( InstMatch, lookupInstEnv )
 import FamInstEnv  ( isDominatedBy, injectiveBranches,
@@ -149,7 +151,7 @@ The nested forall is ambiguous.  Originally we called checkAmbiguity
 in the forall case of check_type, but that had two bad consequences:
   * We got two error messages about (Eq b) in a nested forall like this:
        g :: forall a. Eq a => forall b. Eq b => a -> a
-  * If we try to check for ambiguity of an nested forall like
+  * If we try to check for ambiguity of a nested forall like
     (forall a. Eq a => b), the implication constraint doesn't bind
     all the skolems, which results in "No skolem info" in error
     messages (see Trac #10432).
@@ -225,6 +227,7 @@ wantAmbiguityCheck ctxt
   = case ctxt of  -- See Note [When we don't check for ambiguity]
       GhciCtxt     -> False
       TySynCtxt {} -> False
+      TypeAppCtxt  -> False
       _            -> True
 
 checkUserTypeError :: Type -> TcM ()
@@ -269,6 +272,10 @@ In a few places we do not want to check a user-specified type for ambiguity
   from doing an ambiguity check on a type with TyVars in it.  Fixing this
   would not be hard, but let's wait till there's a reason.
 
+* TypeAppCtxt: visible type application
+     f @ty
+  No need to check ty for ambiguity
+
 
 ************************************************************************
 *                                                                      *
@@ -720,19 +727,25 @@ check_pred_help under_syn env dflags ctxt pred
   | Just pred' <- tcView pred  -- Switch on under_syn when going under a
                                  -- synonym (Trac #9838, yuk)
   = check_pred_help True env dflags ctxt pred'
-  | otherwise
+
+  | otherwise  -- A bit like classifyPredType, but not the same
+               -- E.g. we treat (~) like (~#); and we look inside tuples
   = case splitTyConApp_maybe pred of
       Just (tc, tys)
         | isTupleTyCon tc
         -> check_tuple_pred under_syn env dflags ctxt pred tys
-           -- NB: this equality check must come first, because (~) is a class,
-           -- too.
+
         | tc `hasKey` heqTyConKey ||
           tc `hasKey` eqTyConKey ||
           tc `hasKey` eqPrimTyConKey
+          -- NB: this equality check must come first,
+          --  because (~) is a class,too.
         -> check_eq_pred env dflags pred tc tys
+
         | Just cls <- tyConClass_maybe tc
-        -> check_class_pred env dflags ctxt pred cls tys  -- Includes Coercible
+          -- Includes Coercible
+        -> check_class_pred env dflags ctxt pred cls tys
+
       _ -> check_irred_pred under_syn env dflags ctxt pred
 
 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TyCon -> [TcType] -> TcM ()
@@ -908,6 +921,7 @@ okIPCtxt (InstDeclCtxt {}) = False
 okIPCtxt (SpecInstCtxt {}) = False
 okIPCtxt (RuleSigCtxt {})  = False
 okIPCtxt DefaultDeclCtxt   = False
+okIPCtxt DerivClauseCtxt   = False
 
 {-
 Note [Kind polymorphic type classes]
@@ -1037,9 +1051,9 @@ checkValidInstHead ctxt clas cls_args
              checkHasFieldInst clas cls_args
 
            -- Check language restrictions;
-           -- but not for SPECIALISE instance pragmas
+           -- but not for SPECIALISE instance pragmas or deriving clauses
        ; let ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args
-       ; unless spec_inst_prag $
+       ; unless (spec_inst_prag || deriv_clause) $
          do { checkTc (xopt LangExt.TypeSynonymInstances dflags ||
                        all tcInstHeadTyNotSynonym ty_args)
                  (instTypeErr clas cls_args head_type_synonym_msg)
@@ -1055,6 +1069,7 @@ checkValidInstHead ctxt clas cls_args
        ; mapM_ checkValidTypePat ty_args }
   where
     spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False }
+    deriv_clause   = case ctxt of { DerivClauseCtxt -> True; _ -> False }
 
     head_type_synonym_msg = parens (
                 text "All instance types must be of the form (T t1 ... tn)" $$
@@ -1105,7 +1120,7 @@ dropCasts :: Type -> Type
 -- See Note [Casts during validity checking]
 -- This function can turn a well-kinded type into an ill-kinded
 -- one, so I've kept it local to this module
--- To consider: drop only UnivCo(HoleProv) casts
+-- To consider: drop only HoleCo casts
 dropCasts (CastTy ty _)     = dropCasts ty
 dropCasts (AppTy t1 t2)     = mkAppTy (dropCasts t1) (dropCasts t2)
 dropCasts (FunTy t1 t2)     = mkFunTy (dropCasts t1) (dropCasts t2)
@@ -1555,8 +1570,8 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
        ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
 
        -- And now kind args
-       ; checkTc (all check_arg kind_shapes)
-                 (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
+       ; checkTcM (all check_arg kind_shapes)
+                  (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
 
        ; traceTc "cfi" (vcat [ ppr inst_tvs
                              , ppr arg_shapes
@@ -1585,7 +1600,16 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
                vcat [ text "where the `<tv>' arguments are type variables,"
                     , text "distinct from each other and from the instance variables" ] ]
 
-    expected_args = [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ]
+    -- We need to tidy, since it's possible that expected_args will contain
+    -- inferred kind variables with names identical to those in at_tys. If we
+    -- don't, we'll end up with horrible messages like this one (#13972):
+    --
+    --   Expected: T (a -> Either a b)
+    --     Actual: T (a -> Either a b)
+    (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
+    (tidy_env2, expected_args)
+      = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
+                                | (exp_ty, at_ty) <- arg_shapes ]
     mk_tv at_ty   = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
     tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
 
@@ -1614,7 +1638,7 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
        ; foldlM_ check_branch_compat [] branch_list }
   where
     branch_list = fromBranches branches
-    injectivity = familyTyConInjectivityInfo fam_tc
+    injectivity = tyConInjectivityInfo fam_tc
 
     check_branch_compat :: [CoAxBranch]    -- previous branches in reverse order
                         -> CoAxBranch      -- current branch
@@ -1762,10 +1786,6 @@ checkValidTypePat pat_ty
        ; checkTc (isTyFamFree pat_ty) $
          tyFamInstIllegalErr pat_ty }
 
-isTyFamFree :: Type -> Bool
--- ^ Check that a type does not contain any type family applications.
-isTyFamFree = null . tcTyFamInsts
-
 -- Error messages
 
 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
@@ -1959,13 +1979,13 @@ fvCo (CoherenceCo co1 co2)  = fvCo co1 ++ fvCo co2
 fvCo (KindCo co)            = fvCo co
 fvCo (SubCo co)             = fvCo co
 fvCo (AxiomRuleCo _ cs)     = concatMap fvCo cs
+fvCo (HoleCo h)             = pprPanic "fvCo falls into a hole" (ppr h)
 
 fvProv :: UnivCoProvenance -> [TyCoVar]
 fvProv UnsafeCoerceProv    = []
 fvProv (PhantomProv co)    = fvCo co
 fvProv (ProofIrrelProv co) = fvCo co
 fvProv (PluginProv _)      = []
-fvProv (HoleProv h)        = pprPanic "fvProv falls into a hole" (ppr h)
 
 sizeType :: Type -> Int
 -- Size of a type: the number of variables and constructors