<commit_before>%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

\begin{code}
module TcValidity (
  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
  expectedKindInCtxt, 
  checkValidTheta, checkValidFamPats,
  checkValidInstance, validDerivPred,
  checkInstTermination, checkValidTyFamInst, checkTyFamFreeness, 
  checkConsistentFamInst,
  arityErr, badATErr
  ) where

#include "HsVersions.h"

-- friends:
import TcUnify    ( tcSubType )
import TcSimplify ( simplifyTop )
import TypeRep
import TcType
import TcMType
import Type
import Unify( tcMatchTyX )
import Kind
import CoAxiom
import Class
import TyCon

-- others:
import HsSyn            -- HsType
import TcRnMonad        -- TcType, amongst others
import FunDeps
import Name
import VarEnv
import VarSet
import ErrUtils
import PrelNames
import DynFlags
import Util
import Maybes
import ListSetOps
import SrcLoc
import Outputable
import FastString
import BasicTypes ( Arity )

import Control.Monad
import Data.List        ( (\\) )
\end{code}
 

%************************************************************************
%*                                                                      *
          Checking for ambiguity
%*                                                                      *
%************************************************************************


\begin{code}
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity ctxt ty
  | GhciCtxt <- ctxt    -- Allow ambiguous types in GHCi's :kind command
  = return ()           -- E.g.   type family T a :: *  -- T :: forall k. k -> *
                        -- Then :k T should work in GHCi, not complain that
                        -- (T k) is ambiguous!

  | otherwise
  = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
       ; unless allow_ambiguous $ 
    do {(subst, _tvs) <- tcInstSkolTyVars (varSetElems (tyVarsOfType ty))
       ; let ty' = substTy subst ty  
              -- The type might have free TyVars,
              -- so we skolemise them as TcTyVars
              -- Tiresome; but the type inference engine expects TcTyVars
       ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
                            captureConstraints $
                            tcSubType (AmbigOrigin ctxt) ctxt ty' ty'

         -- Solve the constraints eagerly because an ambiguous type
         -- can cause a cascade of further errors.  The free tyvars
         -- are skolemised, so we can safely use tcSimplifyTop
       ; _ev_binds <- simplifyTop wanted

       ; return () } } 
 where
   mk_msg ty tidy_env 
     = return (tidy_env', msg)
     where
       (tidy_env', tidy_ty) = tidyOpenType tidy_env ty
       msg = hang (ptext (sLit "In the ambiguity check for:"))
                2 (ppr tidy_ty)
\end{code}


%************************************************************************
%*                                                                      *
          Checking validity of a user-defined type
%*                                                                      *
%************************************************************************

When dealing with a user-written type, we first translate it from an HsType
to a Type, performing kind checking, and then check various things that should 
be true about it.  We don't want to perform these checks at the same time
as the initial translation because (a) they are unnecessary for interface-file
types and (b) when checking a mutually recursive group of type and class decls,
we can't "look" at the tycons/classes yet.  Also, the checks are are rather
diverse, and used to really mess up the other code.

One thing we check for is 'rank'.  

        Rank 0:         monotypes (no foralls)
        Rank 1:         foralls at the front only, Rank 0 inside
        Rank 2:         foralls at the front, Rank 1 on left of fn arrow,

        basic ::= tyvar | T basic ... basic

        r2  ::= forall tvs. cxt => r2a
        r2a ::= r1 -> r2a | basic
        r1  ::= forall tvs. cxt => r0
        r0  ::= r0 -> r0 | basic
        
Another thing is to check that type synonyms are saturated. 
This might not necessarily show up in kind checking.
        type A i = i
        data T k = MkT (k Int)
        f :: T A        -- BAD!

        
\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
-- Not used for instance decls; checkValidInstance instead
checkValidType ctxt ty 
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
       ; rankn_flag  <- xoptM Opt_RankNTypes
       ; let gen_rank :: Rank -> Rank
             gen_rank r | rankn_flag = ArbitraryRank
                        | otherwise  = r

             rank1 = gen_rank r1
             rank0 = gen_rank r0

             r0 = rankZeroMonoType
             r1 = LimitedRank True r0

             rank
               = case ctxt of
                 DefaultDeclCtxt-> MustBeMonoType
                 ResSigCtxt     -> MustBeMonoType
                 LamPatSigCtxt  -> rank0
                 BindPatSigCtxt -> rank0
                 RuleSigCtxt _  -> rank1
                 TySynCtxt _    -> rank0

                 ExprSigCtxt    -> rank1
                 FunSigCtxt _   -> rank1
                 InfSigCtxt _   -> ArbitraryRank        -- Inferred type
                 ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                         -- constructor, hence rank 1

                 ForSigCtxt _   -> rank1
                 SpecInstCtxt   -> rank1
                 ThBrackCtxt    -> rank1
                 GhciCtxt       -> ArbitraryRank
                 _              -> panic "checkValidType"
                                          -- Can't happen; not used for *user* sigs

        -- Check the internal validity of the type itself
       ; check_type ctxt rank ty

        -- Check that the thing has kind Type, and is lifted if necessary
        -- Do this second, because we can't usefully take the kind of an 
        -- ill-formed type such as (a~Int)
       ; check_kind ctxt ty }

checkValidMonoType :: Type -> TcM ()
checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty


check_kind :: UserTypeCtxt -> TcType -> TcM ()
-- Check that the type's kind is acceptable for the context
check_kind ctxt ty
  | TySynCtxt {} <- ctxt
  = do { ck <- xoptM Opt_ConstraintKinds
       ; unless ck $
         checkTc (not (returnsConstraintKind actual_kind)) 
                 (constraintSynErr actual_kind) }

  | Just k <- expectedKindInCtxt ctxt
  = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)

  | otherwise
  = return ()   -- Any kind will do
  where
    actual_kind = typeKind ty

-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
expectedKindInCtxt ThBrackCtxt    = Nothing
expectedKindInCtxt GhciCtxt       = Nothing<commit_msg>Improve debug tracing a bit<commit_after>%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

\begin{code}
module TcValidity (
  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
  expectedKindInCtxt, 
  checkValidTheta, checkValidFamPats,
  checkValidInstance, validDerivPred,
  checkInstTermination, checkValidTyFamInst, checkTyFamFreeness, 
  checkConsistentFamInst,
  arityErr, badATErr
  ) where

#include "HsVersions.h"

-- friends:
import TcUnify    ( tcSubType )
import TcSimplify ( simplifyTop )
import TypeRep
import TcType
import TcMType
import Type
import Unify( tcMatchTyX )
import Kind
import CoAxiom
import Class
import TyCon

-- others:
import HsSyn            -- HsType
import TcRnMonad        -- TcType, amongst others
import FunDeps
import Name
import VarEnv
import VarSet
import ErrUtils
import PrelNames
import DynFlags
import Util
import Maybes
import ListSetOps
import SrcLoc
import Outputable
import FastString
import BasicTypes ( Arity )

import Control.Monad
import Data.List        ( (\\) )
\end{code}
 

%************************************************************************
%*                                                                      *
          Checking for ambiguity
%*                                                                      *
%************************************************************************


\begin{code}
checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
checkAmbiguity ctxt ty
  | GhciCtxt <- ctxt    -- Allow ambiguous types in GHCi's :kind command
  = return ()           -- E.g.   type family T a :: *  -- T :: forall k. k -> *
                        -- Then :k T should work in GHCi, not complain that
                        -- (T k) is ambiguous!

  | otherwise
  = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
       ; unless allow_ambiguous $ 
    do { traceTc "Ambiguity check for" (ppr ty)
       ; (subst, _tvs) <- tcInstSkolTyVars (varSetElems (tyVarsOfType ty))
       ; let ty' = substTy subst ty  
              -- The type might have free TyVars,
              -- so we skolemise them as TcTyVars
              -- Tiresome; but the type inference engine expects TcTyVars

         -- Solve the constraints eagerly because an ambiguous type
         -- can cause a cascade of further errors.  Since the free 
         -- tyvars are skolemised, we can safely use tcSimplifyTop
       ; addErrCtxtM (mk_msg ty') $
         do { (_wrap, wanted) <- captureConstraints $
                                 tcSubType (AmbigOrigin ctxt) ctxt ty' ty'
            ; _ev_binds <- simplifyTop wanted
            ; return () }

       ; traceTc "Done ambiguity check for" (ppr ty) } }
 where
   mk_msg ty tidy_env 
     = return (tidy_env', msg)
     where
       (tidy_env', tidy_ty) = tidyOpenType tidy_env ty
       msg = hang (ptext (sLit "In the ambiguity check for:"))
                2 (ppr tidy_ty)
\end{code}


%************************************************************************
%*                                                                      *
          Checking validity of a user-defined type
%*                                                                      *
%************************************************************************

When dealing with a user-written type, we first translate it from an HsType
to a Type, performing kind checking, and then check various things that should 
be true about it.  We don't want to perform these checks at the same time
as the initial translation because (a) they are unnecessary for interface-file
types and (b) when checking a mutually recursive group of type and class decls,
we can't "look" at the tycons/classes yet.  Also, the checks are are rather
diverse, and used to really mess up the other code.

One thing we check for is 'rank'.  

        Rank 0:         monotypes (no foralls)
        Rank 1:         foralls at the front only, Rank 0 inside
        Rank 2:         foralls at the front, Rank 1 on left of fn arrow,

        basic ::= tyvar | T basic ... basic

        r2  ::= forall tvs. cxt => r2a
        r2a ::= r1 -> r2a | basic
        r1  ::= forall tvs. cxt => r0
        r0  ::= r0 -> r0 | basic
        
Another thing is to check that type synonyms are saturated. 
This might not necessarily show up in kind checking.
        type A i = i
        data T k = MkT (k Int)
        f :: T A        -- BAD!

        
\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
-- Not used for instance decls; checkValidInstance instead
checkValidType ctxt ty 
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
       ; rankn_flag  <- xoptM Opt_RankNTypes
       ; let gen_rank :: Rank -> Rank
             gen_rank r | rankn_flag = ArbitraryRank
                        | otherwise  = r

             rank1 = gen_rank r1
             rank0 = gen_rank r0

             r0 = rankZeroMonoType
             r1 = LimitedRank True r0

             rank
               = case ctxt of
                 DefaultDeclCtxt-> MustBeMonoType
                 ResSigCtxt     -> MustBeMonoType
                 LamPatSigCtxt  -> rank0
                 BindPatSigCtxt -> rank0
                 RuleSigCtxt _  -> rank1
                 TySynCtxt _    -> rank0

                 ExprSigCtxt    -> rank1
                 FunSigCtxt _   -> rank1
                 InfSigCtxt _   -> ArbitraryRank        -- Inferred type
                 ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                         -- constructor, hence rank 1

                 ForSigCtxt _   -> rank1
                 SpecInstCtxt   -> rank1
                 ThBrackCtxt    -> rank1
                 GhciCtxt       -> ArbitraryRank
                 _              -> panic "checkValidType"
                                          -- Can't happen; not used for *user* sigs

        -- Check the internal validity of the type itself
       ; check_type ctxt rank ty

        -- Check that the thing has kind Type, and is lifted if necessary
        -- Do this second, because we can't usefully take the kind of an 
        -- ill-formed type such as (a~Int)
       ; check_kind ctxt ty
       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }

checkValidMonoType :: Type -> TcM ()
checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty


check_kind :: UserTypeCtxt -> TcType -> TcM ()
-- Check that the type's kind is acceptable for the context
check_kind ctxt ty
  | TySynCtxt {} <- ctxt
  = do { ck <- xoptM Opt_ConstraintKinds
       ; unless ck $
         checkTc (not (returnsConstraintKind actual_kind)) 
                 (constraintSynErr actual_kind) }

  | Just k <- expectedKindInCtxt ctxt
  = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)

  | otherwise
  = return ()   -- Any kind will do
  where
    actual_kind = typeKind ty

-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
expectedKindInCtxt ThBrackCtxt    = Nothing
expectedKindInCtxt GhciCtxt       = Nothing
{'fraction_non_alphanumeric': 0.10762115145657876, 'fraction_numerical': 0.006350959547148972, 'mean_word_length': 1.9113745980707395, 'pattern_counts': {'":': 3, '<': 27, '<?xml version=': 0, '>': 67, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 27, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2742527', 'n_tokens_mistral': 4155, 'n_tokens_neox': 3903, 'n_words': 1424}