TcTyClsDecls.hs 207 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1996-1998

5 6

TcTyClsDecls: Typecheck type and class declarations
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables, MultiWayIf #-}
10
{-# LANGUAGE TypeFamilies #-}
11
{-# LANGUAGE ViewPatterns #-}
Ian Lynagh's avatar
Ian Lynagh committed
12

13 14
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

15
module TcTyClsDecls (
16
        tcTyAndClassDecls,
17

18 19
        -- Functions used by TcInstDcls to check
        -- data/type family instance declarations
20
        kcConDecls, tcConDecls, dataDeclChecks, checkValidTyCon,
21
        tcFamTyPats, tcTyFamInstEqn,
22
        tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
23
        unravelFamInstPats, addConsistencyConstraints,
24
        wrongKindOfFamily
25 26
    ) where

27
#include "HsVersions.h"
28

29 30
import GhcPrelude

31
import GHC.Hs
Sylvain Henry's avatar
Sylvain Henry committed
32
import GHC.Driver.Types
33
import BuildTyCl
34
import TcRnMonad
35
import TcEnv
36
import TcValidity
37
import TcHsSyn
38 39
import TcTyDecls
import TcClassDcl
40
import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
41
import TcDeriv (DerivInfo(..))
42
import TcUnify ( checkTvConstraints )
43
import TcHsType
44
import ClsInst( AssocInstInfo(..) )
45
import TcMType
46
import TysWiredIn ( unitTy, makeRecoveryTyCon )
47
import TcType
48
import GHC.Rename.Env( lookupConstructorFields )
49
import FamInst
Sylvain Henry's avatar
Sylvain Henry committed
50 51
import GHC.Core.FamInstEnv
import GHC.Core.Coercion
52
import TcOrigin
Sylvain Henry's avatar
Sylvain Henry committed
53 54 55 56 57 58 59
import GHC.Core.Type
import GHC.Core.TyCo.Rep   -- for checkValidRoles
import GHC.Core.TyCo.Ppr( pprTyVars, pprWithExplicitKindsWhen )
import GHC.Core.Class
import GHC.Core.Coercion.Axiom
import GHC.Core.TyCon
import GHC.Core.DataCon
Sylvain Henry's avatar
Sylvain Henry committed
60 61 62 63 64 65 66 67
import GHC.Types.Id
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Module
import GHC.Types.Name
import GHC.Types.Name.Set
import GHC.Types.Name.Env
sof's avatar
sof committed
68
import Outputable
69
import Maybes
Sylvain Henry's avatar
Sylvain Henry committed
70
import GHC.Core.Unify
71
import Util
Sylvain Henry's avatar
Sylvain Henry committed
72
import GHC.Types.SrcLoc
73
import ListSetOps
Sylvain Henry's avatar
Sylvain Henry committed
74
import GHC.Driver.Session
Sylvain Henry's avatar
Sylvain Henry committed
75
import GHC.Types.Unique
Sylvain Henry's avatar
Sylvain Henry committed
76
import GHC.Core.ConLike( ConLike(..) )
Sylvain Henry's avatar
Sylvain Henry committed
77
import GHC.Types.Basic
78
import qualified GHC.LanguageExtensions as LangExt
79

80
import Control.Monad
81
import Data.Foldable
82
import Data.Function ( on )
83
import Data.Functor.Identity
84
import Data.List
85
import qualified Data.List.NonEmpty as NE
86
import Data.List.NonEmpty ( NonEmpty(..) )
87
import qualified Data.Set as Set
88
import Data.Tuple( swap )
89

Austin Seipp's avatar
Austin Seipp committed
90 91 92
{-
************************************************************************
*                                                                      *
93
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
94 95
*                                                                      *
************************************************************************
96

dreixel's avatar
dreixel committed
97 98 99 100 101 102 103 104 105 106 107 108 109
Note [Grouping of type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
connected component of mutually dependent types and classes. We kind check and
type check each group separately to enhance kind polymorphism. Take the
following example:

  type Id a = a
  data X = X (Id Int)

If we were to kind check the two declarations together, we would give Id the
kind * -> *, since we apply it to an Int in the definition of X. But we can do
better than that, since Id really is kind polymorphic, and should get kind
110
forall (k::*). k -> k. Since it does not depend on anything else, it can be
dreixel's avatar
dreixel committed
111 112 113 114
kind-checked by itself, hence getting the most general kind. We then kind check
X, which works fine because we then know the polymorphic kind of Id, and simply
instantiate k to *.

115 116 117 118 119 120 121 122 123
Note [Check role annotations in a second pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Role inference potentially depends on the types of all of the datacons declared
in a mutually recursive group. The validity of a role annotation, in turn,
depends on the result of role inference. Because the types of datacons might
be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
*all* the tycons in a group for validity before checking *any* of the roles.
Thus, we take two passes over the resulting tycons, first checking for general
validity and then checking for valid role annotations.
Austin Seipp's avatar
Austin Seipp committed
124
-}
125

126
tcTyAndClassDecls :: [TyClGroup GhcRn]      -- Mutually-recursive groups in
127 128 129 130
                                            -- dependency order
                  -> TcM ( TcGblEnv         -- Input env extended by types and
                                            -- classes
                                            -- and their implicit Ids,DataCons
131
                         , [InstInfo GhcRn] -- Source-code instance decls info
132
                         , [DerivInfo]      -- Deriving info
133
                         )
134
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
135
tcTyAndClassDecls tyclds_s
136 137 138 139
  -- The code recovers internally, but if anything gave rise to
  -- an error we'd better stop now, to avoid a cascade
  -- Type check each group in dependency order folding the global env
  = checkNoErrs $ fold_env [] [] tyclds_s
dreixel's avatar
dreixel committed
140
  where
141
    fold_env :: [InstInfo GhcRn]
142
             -> [DerivInfo]
143 144
             -> [TyClGroup GhcRn]
             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
145 146 147 148 149 150 151 152 153 154 155
    fold_env inst_info deriv_info []
      = do { gbl_env <- getGblEnv
           ; return (gbl_env, inst_info, deriv_info) }
    fold_env inst_info deriv_info (tyclds:tyclds_s)
      = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
           ; setGblEnv tcg_env $
               -- remaining groups are typechecked in the extended global env.
             fold_env (inst_info' ++ inst_info)
                      (deriv_info' ++ deriv_info)
                      tyclds_s }

156 157
tcTyClGroup :: TyClGroup GhcRn
            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
158
-- Typecheck one strongly-connected component of type, class, and instance decls
159
-- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
160 161
tcTyClGroup (TyClGroup { group_tyclds = tyclds
                       , group_roles  = roles
162
                       , group_kisigs = kisigs
163 164 165
                       , group_instds = instds })
  = do { let role_annots = mkRoleAnnotEnv roles

166
           -- Step 1: Typecheck the standalone kind signatures and type/class declarations
167
       ; traceTc "---- tcTyClGroup ---- {" empty
168
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
169 170 171 172
       ; (tyclss, data_deriv_info) <-
           tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution]
           do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs
              ; tcTyClDecls tyclds kisig_env role_annots }
173

174 175 176 177 178 179
           -- Step 1.5: Make sure we don't have any type synonym cycles
       ; traceTc "Starting synonym cycle check" (ppr tyclss)
       ; this_uid <- fmap thisPackage getDynFlags
       ; checkSynCycles this_uid tyclss tyclds
       ; traceTc "Done synonym cycle check" (ppr tyclss)

180 181 182 183 184
           -- Step 2: Perform the validity check on those types/classes
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 3 (adding implicit things) because the latter
           -- expects well-formed TyCons
       ; traceTc "Starting validity check" (ppr tyclss)
185
       ; tyclss <- concatMapM checkValidTyCl tyclss
186 187 188 189
       ; traceTc "Done validity check" (ppr tyclss)
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]

190 191
       ; traceTc "---- end tcTyClGroup ---- }" empty

192 193 194
           -- Step 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
195 196 197
       ; gbl_env <- addTyConsToGblEnv tyclss

           -- Step 4: check instance declarations
198 199 200 201 202 203 204
       ; (gbl_env', inst_info, datafam_deriv_info) <-
         setGblEnv gbl_env $
         tcInstDecls1 instds

       ; let deriv_info = datafam_deriv_info ++ data_deriv_info
       ; return (gbl_env', inst_info, deriv_info) }

205

206
tcTyClGroup (XTyClGroup nec) = noExtCon nec
207

208 209 210
-- Gives the kind for every TyCon that has a standalone kind signature
type KindSigEnv = NameEnv Kind

211 212
tcTyClDecls
  :: [LTyClDecl GhcRn]
213
  -> KindSigEnv
214 215
  -> RoleAnnotEnv
  -> TcM ([TyCon], [DerivInfo])
216 217
tcTyClDecls tyclds kisig_env role_annots
  = do {    -- Step 1: kind-check this group and returns the final
dreixel's avatar
dreixel committed
218 219
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
220
         tc_tycons <- kcTyClGroup kisig_env tyclds
221
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
222

223 224
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
225 226 227 228
            --
            -- NB: We have to be careful here to NOT eagerly unfold
            -- type synonyms, as we have not tested for type synonym
            -- loops yet and could fall into a black hole.
229
       ; fixM $ \ ~(rec_tyclss, _) -> do
230 231
           { tcg_env <- getGblEnv
           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
dreixel's avatar
dreixel committed
232 233 234

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
235
                 -- (see Note [Recursion and promoting data constructors])
236
                 -- we will have failed already in kcTyClGroup, so no worries here
237 238
           ; (tycons, data_deriv_infos) <-
             tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
dreixel's avatar
dreixel committed
239 240

                 -- Also extend the local type envt with bindings giving
241
                 -- a TcTyCon for each each knot-tied TyCon or Class
242
                 -- See Note [Type checking recursive type and class declarations]
243 244
                 -- and Note [Type environment evolution]
             tcExtendKindEnvWithTyCons tc_tycons $
dreixel's avatar
dreixel committed
245 246

                 -- Kind and type check declarations for this group
247 248
               mapAndUnzipM (tcTyClDecl roles) tyclds
           ; return (tycons, concat data_deriv_infos)
249
           } }
250 251 252
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
253 254
                                  , ppr (tyConResKind tc)
                                  , ppr (isTcTyCon tc) ])
dreixel's avatar
dreixel committed
255

256
zipRecTyClss :: [TcTyCon]
257
             -> [TyCon]           -- Knot-tied
258
             -> [(Name,TyThing)]
259 260
-- Build a name-TyThing mapping for the TyCons bound by decls
-- being careful not to look at the knot-tied [TyThing]
batterseapower's avatar
batterseapower committed
261
-- The TyThings in the result list must have a visible ATyCon,
262 263
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
264 265
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
266
  where
267 268
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
269

270 271 272 273 274 275 276 277 278
    add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)

    add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_one_tc tc env = extendNameEnv env (tyConName tc) tc

    get name = case lookupNameEnv rec_tc_env name of
                 Just tc -> tc
                 other   -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
279

Austin Seipp's avatar
Austin Seipp committed
280 281 282
{-
************************************************************************
*                                                                      *
283
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
284 285
*                                                                      *
************************************************************************
286

287 288 289 290
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

291 292
   1. Make up a kind variable for each parameter of the declarations,
      and extend the kind environment (which is in the TcLclEnv)
293

294
   2. Kind check the declarations
295

296 297
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
298

299 300
  class C a where
     op :: D b => a -> b -> b
301

302 303
  class D c where
     bop :: (Monad c) => ...
304 305 306 307 308

Here, the kind of the locally-polymorphic type variable "b"
depends on *all the uses of class D*.  For example, the use of
Monad c in bop's type signature means that D must have kind Type->Type.

309 310 311 312 313 314
Note: we don't treat type synonyms specially (we used to, in the past);
in particular, even if we have a type synonym cycle, we still kind check
it normally, and test for cycles later (checkSynCycles).  The reason
we can get away with this is because we have more systematic TYPE r
inference, which means that we can do unification between kinds that
aren't lifted (this historically was not true.)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
315

316
The downside of not directly reading off the kinds of the RHS of
317 318 319 320
type synonyms in topological order is that we don't transparently
support making synonyms of types with higher-rank kinds.  But
you can always specify a CUSK directly to make this work out.
See tc269 for an example.
321

322 323
Note [CUSKs and PolyKinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~
324 325 326 327 328
Consider

    data T (a :: *) = MkT (S a)   -- Has CUSK
    data S a = MkS (T Int) (S a)  -- No CUSK

329
Via inferInitialKinds we get
330 331 332 333 334 335 336 337 338 339 340 341
  T :: * -> *
  S :: kappa -> *

Then we call kcTyClDecl on each decl in the group, to constrain the
kind unification variables.  BUT we /skip/ the RHS of any decl with
a CUSK.  Here we skip the RHS of T, so we eventually get
  S :: forall k. k -> *

This gets us more polymorphism than we would otherwise get, similar
(but implemented strangely differently from) the treatment of type
signatures in value declarations.

342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
However, we only want to do so when we have PolyKinds.
When we have NoPolyKinds, we don't skip those decls, because we have defaulting
(#16609). Skipping won't bring us more polymorphism when we have defaulting.
Consider

  data T1 a = MkT1 T2        -- No CUSK
  data T2 = MkT2 (T1 Maybe)  -- Has CUSK

If we skip the rhs of T2 during kind-checking, the kind of a remains unsolved.
With PolyKinds, we do generalization to get T1 :: forall a. a -> *. And the
program type-checks.
But with NoPolyKinds, we do defaulting to get T1 :: * -> *. Defaulting happens
in quantifyTyVars, which is called from generaliseTcTyCon. Then type-checking
(T1 Maybe) will throw a type error.

Summary: with PolyKinds, we must skip; with NoPolyKinds, we must /not/ skip.

359 360
Open type families
~~~~~~~~~~~~~~~~~~
361 362 363
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

364
The kind of an open type family is solely determinded by its kind signature;
365
hence, only kind signatures participate in the construction of the initial
366
kind environment (as constructed by `inferInitialKind'). In fact, we ignore
367 368 369
instances of families altogether in the following. However, we need to include
the kinds of *associated* families into the construction of the initial kind
environment. (This is handled by `allDecls').
370 371 372

See also Note [Kind checking recursive type and class declarations]

373
Note [How TcTyCons work]
374
~~~~~~~~~~~~~~~~~~~~~~~~
375 376 377 378 379 380 381 382 383 384
TcTyCons are used for two distinct purposes

1.  When recovering from a type error in a type declaration,
    we want to put the erroneous TyCon in the environment in a
    way that won't lead to more errors.  We use a TcTyCon for this;
    see makeRecoveryTyCon.

2.  When checking a type/class declaration (in module TcTyClsDecls), we come
    upon knowledge of the eventual tycon in bits and pieces.

385
      S1) First, we use inferInitialKinds to look over the user-provided
386 387 388 389
          kind signature of a tycon (including, for example, the number
          of parameters written to the tycon) to get an initial shape of
          the tycon's kind.  We record that shape in a TcTyCon.

Tobias Dammers's avatar
Tobias Dammers committed
390 391 392 393
          For CUSK tycons, the TcTyCon has the final, generalised kind.
          For non-CUSK tycons, the TcTyCon has as its tyConBinders only
          the explicit arguments given -- no kind variables, etc.

394 395 396 397
      S2) Then, using these initial kinds, we kind-check the body of the
          tycon (class methods, data constructors, etc.), filling in the
          metavariables in the tycon's initial kind.

Tobias Dammers's avatar
Tobias Dammers committed
398
      S3) We then generalize to get the (non-CUSK) tycon's final, fixed
399 400 401 402 403 404 405 406
          kind. Finally, once this has happened for all tycons in a
          mutually recursive group, we can desugar the lot.

    For convenience, we store partially-known tycons in TcTyCons, which
    might store meta-variables. These TcTyCons are stored in the local
    environment in TcTyClsDecls, until the real full TyCons can be created
    during desugaring. A desugared program should never have a TcTyCon.

407 408 409 410
3.  In a TcTyCon, everything is zonked after the kind-checking pass (S2).

4.  tyConScopedTyVars.  A challenging piece in all of this is that we
    end up taking three separate passes over every declaration:
411
      - one in inferInitialKind (this pass look only at the head, not the body)
412 413
      - one in kcTyClDecls (to kind-check the body)
      - a final one in tcTyClDecls (to desugar)
414

415 416 417 418 419
    In the latter two passes, we need to connect the user-written type
    variables in an LHsQTyVars with the variables in the tycon's
    inferred kind. Because the tycon might not have a CUSK, this
    matching up is, in general, quite hard to do.  (Look through the
    git history between Dec 2015 and Apr 2016 for
420 421 422 423
    TcHsType.splitTelescopeTvs!)

    Instead of trying, we just store the list of type variables to
    bring into scope, in the tyConScopedTyVars field of the TcTyCon.
424
    These tyvars are brought into scope in TcHsType.bindTyClTyVars.
425

426 427 428 429 430 431 432 433
    In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
    than just [TcTyVar]?  Consider these mutually-recursive decls
       data T (a :: k1) b = MkT (S a b)
       data S (c :: k2) d = MkS (T c d)
    We start with k1 bound to kappa1, and k2 to kappa2; so initially
    in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But
    then kappa1 and kappa2 get unified; so after the zonking in
    'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ.
434

435
See also Note [Type checking recursive type and class declarations].
436

437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538
Note [Swizzling the tyvars before generaliseTcTyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This Note only applies when /inferring/ the kind of a TyCon.
If there is a separate kind signature, or a CUSK, we take an entirely
different code path.

For inference, consider
   class C (f :: k) x where
      type T f
      op :: D f => blah
   class D (g :: j) y where
      op :: C g => y -> blah

Here C and D are considered mutually recursive.  Neither has a CUSK.
Just before generalisation we have the (un-quantified) kinds
   C :: k1 -> k2 -> Constraint
   T :: k1 -> Type
   D :: k1 -> Type -> Constraint
Notice that f's kind and g's kind have been unified to 'k1'. We say
that k1 is the "representative" of k in C's decl, and of j in D's decl.

Now when quantifying, we'd like to end up with
   C :: forall {k2}. forall k. k -> k2 -> Constraint
   T :: forall k. k -> Type
   D :: forall j. j -> Type -> Constraint

That is, we want to swizzle the representative to have the Name given
by the user. Partly this is to improve error messages and the output of
:info in GHCi.  But it is /also/ important because the code for a
default method may mention the class variable(s), but at that point
(tcClassDecl2), we only have the final class tyvars available.
(Alternatively, we could record the scoped type variables in the
TyCon, but it's a nuisance to do so.)

Notes:

* On the input to generaliseTyClDecl, the mapping between the
  user-specified Name and the representative TyVar is recorded in the
  tyConScopedTyVars of the TcTyCon.  NB: you first need to zonk to see
  this representative TyVar.

* The swizzling is actually performed by swizzleTcTyConBndrs

* We must do the swizzling across the whole class decl. Consider
     class C f where
       type S (f :: k)
       type T f
  Here f's kind k is a parameter of C, and its identity is shared
  with S and T.  So if we swizzle the representative k at all, we
  must do so consistently for the entire declaration.

  Hence the call to check_duplicate_tc_binders is in generaliseTyClDecl,
  rather than in generaliseTcTyCon.

There are errors to catch here.  Suppose we had
   class E (f :: j) (g :: k) where
     op :: SameKind f g -> blah

Then, just before generalisation we will have the (unquantified)
   E :: k1 -> k1 -> Constraint

That's bad!  Two distinctly-named tyvars (j and k) have ended up with
the same representative k1.  So when swizzling, we check (in
check_duplicate_tc_binders) that two distinct source names map
to the same representative.

Here's an interesting case:
    class C1 f where
      type S (f :: k1)
      type T (f :: k2)
Here k1 and k2 are different Names, but they end up mapped to the
same representative TyVar.  To make the swizzling consistent (remember
we must have a single k across C1, S and T) we reject the program.

Another interesting case
    class C2 f where
      type S (f :: k) (p::Type)
      type T (f :: k) (p::Type->Type)

Here the two k's (and the two p's) get distinct Uniques, because they
are seen by the renamer as locally bound in S and T resp.  But again
the two (distinct) k's end up bound to the same representative TyVar.
You might argue that this should be accepted, but it's definitely
rejected (via an entirely different code path) if you add a kind sig:
    type C2' :: j -> Constraint
    class C2' f where
      type S (f :: k) (p::Type)
We get
    • Expected kind ‘j’, but ‘f’ has kind ‘k’
    • In the associated type family declaration for ‘S’

So we reject C2 too, even without the kind signature.  We have
to do a bit of work to get a good error message, since both k's
look the same to the user.

Another case
    class C3 (f :: k1) where
      type S (f :: k2)

This will be rejected too.


539 540 541 542 543
Note [Type environment evolution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As we typecheck a group of declarations the type environment evolves.
Consider for example:
  data B (a :: Type) = MkB (Proxy 'MkB)
544

545 546 547 548 549 550 551
We do the following steps:

  1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
     type env with promotion errors
            B   :-> TyConPE
            MkB :-> DataConPE

552
  2. kcTyCLGroup
553
      - Do inferInitialKinds, which will signal a promotion
554
        error if B is used in any of the kinds needed to initialise
555 556
        B's kind (e.g. (a :: Type)) here

557
      - Extend the type env with these initial kinds (monomorphic for
558 559 560 561
        decls that lack a CUSK)
            B :-> TcTyCon <initial kind>
        (thereby overriding the B :-> TyConPE binding)
        and do kcLTyClDecl on each decl to get equality constraints on
562
        all those initial kinds
563

564
      - Generalise the initial kind, making a poly-kinded TcTyCon
565 566 567 568 569

  3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
     TcTyCons, again overriding the promotion-error bindings.

     But note that the data constructor promotion errors are still in place
570
     so that (in our example) a use of MkB will still be signalled as
571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
     an error.

  4. Typecheck the decls.

  5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons


Note [Missed opportunity to retain higher-rank kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In 'kcTyClGroup', there is a missed opportunity to make kind
inference work in a few more cases.  The idea is analogous
to Note [Single function non-recursive binding special-case]:

     * If we have an SCC with a single decl, which is non-recursive,
       instead of creating a unification variable representing the
       kind of the decl and unifying it with the rhs, we can just
       read the type directly of the rhs.

     * Furthermore, we can update our SCC analysis to ignore
       dependencies on declarations which have CUSKs: we don't
       have to kind-check these all at once, since we can use
       the CUSK to initialize the kind environment.

Unfortunately this requires reworking a bit of the code in
'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
596

597 598 599
Note [Don't process associated types in getInitialKind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Previously, we processed associated types in the thing_inside in getInitialKind,
600 601 602 603 604 605 606 607 608 609 610 611
but this was wrong -- we want to do ATs sepearately.
The consequence for not doing it this way is #15142:

  class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
    type ListToTuple as :: Type

We assign k a kind kappa[1]. When checking the tuple (k, Type), we try to unify
kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring
`tuple` into scope. Thus, when we check ListToTuple, kappa[1] still hasn't
unified with Type. And then, when we generalize the kind of ListToTuple (which
indeed has a CUSK, according to the rules), we skolemize the free metavariable
kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple,
612
because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1]
613 614 615 616 617 618
will unify with Type.

Bottom line: as associated types should have no effect on a CUSK enclosing class,
we move processing them to a separate action, run after the outer kind has
been generalized.

619
-}
620

621
kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
622

dreixel's avatar
dreixel committed
623
-- Kind check this group, kind generalize, and return the resulting local env
624
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
625
-- See Note [Kind checking for type and class decls]
626
-- and Note [Inferring kinds for type declarations]
627
kcTyClGroup kisig_env decls
628
  = do  { mod <- getModule
629
        ; traceTc "---- kcTyClGroup ---- {"
630
                  (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
631

632
          -- Kind checking;
633 634 635
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
636 637
          -- See Note [Kind checking for type and class decls]

638 639
        ; cusks_enabled <- xoptM LangExt.CUSKs <&&> xoptM LangExt.PolyKinds
                    -- See Note [CUSKs and PolyKinds]
640 641 642 643 644 645 646 647
        ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls

              get_kind d
                | Just ki <- lookupNameEnv kisig_env (tcdName (unLoc d))
                = Right (d, SAKS ki)

                | cusks_enabled && hsDeclHasCusk (unLoc d)
                = Right (d, CUSK)
648

649
                | otherwise = Left d
650

651 652 653
        ; checked_tcs <- checkInitialKinds kinded_decls
        ; inferred_tcs
            <- tcExtendKindEnvWithTyCons checked_tcs $
654 655 656 657 658
               pushTcLevelM_   $  -- We are going to kind-generalise, so
                                  -- unification variables in here must
                                  -- be one level in
               solveEqualities $
               do {  -- Step 1: Bind kind variables for all decls
659
                    mono_tcs <- inferInitialKinds kindless_decls
660

661 662
                  ; traceTc "kcTyClGroup: initial kinds" $
                    ppr_tc_kinds mono_tcs
Tobias Dammers's avatar
Tobias Dammers committed
663

664 665 666 667 668
                    -- Step 2: Set extended envt, kind-check the decls
                    -- NB: the environment extension overrides the tycon
                    --     promotion-errors bindings
                    --     See Note [Type environment evolution]
                  ; tcExtendKindEnvWithTyCons mono_tcs $
669
                    mapM_ kcLTyClDecl kindless_decls
670 671 672 673

                  ; return mono_tcs }

        -- Step 3: generalisation
Tobias Dammers's avatar
Tobias Dammers committed
674 675 676
        -- Finally, go through each tycon and give it its final kind,
        -- with all the required, specified, and inferred variables
        -- in order.
677 678 679 680
        ; let inferred_tc_env = mkNameEnv $
                                map (\tc -> (tyConName tc, tc)) inferred_tcs
        ; generalized_tcs <- concatMapM (generaliseTyClDecl inferred_tc_env)
                                        kindless_decls
681

682
        ; let poly_tcs = checked_tcs ++ generalized_tcs
683 684
        ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
        ; return poly_tcs }
685
  where
686 687 688
    ppr_tc_kinds tcs = vcat (map pp_tc tcs)
    pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832
type ScopedPairs = [(Name, TcTyVar)]
  -- The ScopedPairs for a TcTyCon are precisely
  --    specified-tvs ++ required-tvs
  -- You can distinguish them because there are tyConArity required-tvs

generaliseTyClDecl :: NameEnv TcTyCon -> LTyClDecl GhcRn -> TcM [TcTyCon]
-- See Note [Swizzling the tyvars before generaliseTcTyCon]
generaliseTyClDecl inferred_tc_env (L _ decl)
  = do { let names_in_this_decl :: [Name]
             names_in_this_decl = tycld_names decl

       -- Extract the specified/required binders and skolemise them
       ; tc_with_tvs  <- mapM skolemise_tc_tycon names_in_this_decl

       -- Zonk, to manifest the side-effects of skolemisation to the swizzler
       -- NB: it's important to skolemise them all before this step. E.g.
       --         class C f where { type T (f :: k) }
       --     We only skolemise k when looking at T's binders,
       --     but k appears in f's kind in C's binders.
       ; tc_infos <- mapM zonk_tc_tycon tc_with_tvs

       -- Swizzle
       ; swizzled_infos <- tcAddDeclCtxt decl (swizzleTcTyConBndrs tc_infos)

       -- And finally generalise
       ; mapAndReportM generaliseTcTyCon swizzled_infos }
  where
    tycld_names :: TyClDecl GhcRn -> [Name]
    tycld_names decl = tcdName decl : at_names decl

    at_names :: TyClDecl GhcRn -> [Name]
    at_names (ClassDecl { tcdATs = ats }) = map (familyDeclName . unLoc) ats
    at_names _ = []  -- Only class decls have associated types

    skolemise_tc_tycon :: Name -> TcM (TcTyCon, ScopedPairs)
    -- Zonk and skolemise the Specified and Required binders
    skolemise_tc_tycon tc_name
      = do { let tc = lookupNameEnv_NF inferred_tc_env tc_name
                      -- This lookup should not fail
           ; scoped_prs <- mapSndM zonkAndSkolemise (tcTyConScopedTyVars tc)
           ; return (tc, scoped_prs) }

    zonk_tc_tycon :: (TcTyCon, ScopedPairs) -> TcM (TcTyCon, ScopedPairs, TcKind)
    zonk_tc_tycon (tc, scoped_prs)
      = do { scoped_prs <- mapSndM zonkTcTyVarToTyVar scoped_prs
                           -- We really have to do this again, even though
                           -- we have just done zonkAndSkolemise
           ; res_kind   <- zonkTcType (tyConResKind tc)
           ; return (tc, scoped_prs, res_kind) }

swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)]
                -> TcM [(TcTyCon, ScopedPairs, TcKind)]
swizzleTcTyConBndrs tc_infos
  | all no_swizzle swizzle_prs
    -- This fast path happens almost all the time
    -- See Note [Non-cloning for tyvar binders] in TcHsType
  = do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos))
       ; return tc_infos }

  | otherwise
  = do { check_duplicate_tc_binders

       ; traceTc "swizzleTcTyConBndrs" $
         vcat [ text "before" <+> ppr_infos tc_infos
              , text "swizzle_prs" <+> ppr swizzle_prs
              , text "after" <+> ppr_infos swizzled_infos ]

       ; return swizzled_infos }

  where
    swizzled_infos =  [ (tc, mapSnd swizzle_var scoped_prs, swizzle_ty kind)
                      | (tc, scoped_prs, kind) <- tc_infos ]

    swizzle_prs :: [(Name,TyVar)]
    -- Pairs the user-specifed Name with its representative TyVar
    -- See Note [Swizzling the tyvars before generaliseTcTyCon]
    swizzle_prs = [ pr | (_, prs, _) <- tc_infos, pr <- prs ]

    no_swizzle :: (Name,TyVar) -> Bool
    no_swizzle (nm, tv) = nm == tyVarName tv

    ppr_infos infos = vcat [ ppr tc <+> pprTyVars (map snd prs)
                           | (tc, prs, _) <- infos ]

    -- Check for duplicates
    -- E.g. data SameKind (a::k) (b::k)
    --      data T (a::k1) (b::k2) = MkT (SameKind a b)
    -- Here k1 and k2 start as TyVarTvs, and get unified with each other
    -- If this happens, things get very confused later, so fail fast
    check_duplicate_tc_binders :: TcM ()
    check_duplicate_tc_binders = unless (null err_prs) $
                                 do { mapM_ report_dup err_prs; failM }

    -------------- Error reporting ------------
    err_prs :: [(Name,Name)]
    err_prs = [ (n1,n2)
              | pr :| prs <- findDupsEq ((==) `on` snd) swizzle_prs
              , (n1,_):(n2,_):_ <- [nubBy ((==) `on` fst) (pr:prs)] ]
              -- This nubBy avoids bogus error reports when we have
              --    [("f", f), ..., ("f",f)....] in swizzle_prs
              -- which happens with  class C f where { type T f }

    report_dup :: (Name,Name) -> TcM ()
    report_dup (n1,n2)
      = setSrcSpan (getSrcSpan n2) $ addErrTc $
        hang (text "Different names for the same type variable:") 2 info
      where
        info | nameOccName n1 /= nameOccName n2
             = quotes (ppr n1) <+> text "and" <+> quotes (ppr n2)
             | otherwise -- Same OccNames! See C2 in
                         -- Note [Swizzling the tyvars before generaliseTcTyCon]
             = vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1)
                    , quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ]

    -------------- The swizzler ------------
    -- This does a deep traverse, simply doing a
    -- Name-to-Name change, governed by swizzle_env
    -- The 'swap' is what gets from the representative TyVar
    -- back to the original user-specified Name
    swizzle_env = mkVarEnv (map swap swizzle_prs)

    swizzleMapper :: TyCoMapper () Identity
    swizzleMapper = TyCoMapper { tcm_tyvar = swizzle_tv
                               , tcm_covar = swizzle_cv
                               , tcm_hole  = swizzle_hole
                               , tcm_tycobinder = swizzle_bndr
                               , tcm_tycon      = swizzle_tycon }
    swizzle_hole  _ hole = pprPanic "swizzle_hole" (ppr hole)
       -- These types are pre-zonked
    swizzle_tycon tc = pprPanic "swizzle_tc" (ppr tc)
       -- TcTyCons can't appear in kinds (yet)
    swizzle_tv _ tv = return (mkTyVarTy (swizzle_var tv))
    swizzle_cv _ cv = return (mkCoVarCo (swizzle_var cv))

    swizzle_bndr _ tcv _
      = return ((), swizzle_var tcv)

    swizzle_var :: Var -> Var
    swizzle_var v
      | Just nm <- lookupVarEnv swizzle_env v
      = updateVarType swizzle_ty (v `setVarName` nm)
      | otherwise
      = updateVarType swizzle_ty v

833 834
    (map_type, _, _, _) = mapTyCo swizzleMapper
    swizzle_ty ty = runIdentity (map_type ty)
835 836 837 838


generaliseTcTyCon :: (TcTyCon, ScopedPairs, TcKind) -> TcM TcTyCon
generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
839 840 841
  -- See Note [Required, Specified, and Inferred for types]
  = setSrcSpan (getSrcSpan tc) $
    addTyConCtxt tc $
842 843 844
    do { -- Step 1: Separate Specified from Required variables
         -- NB: spec_req_tvs = spec_tvs ++ req_tvs
         --     And req_tvs is 1-1 with tyConTyVars
Sylvain Henry's avatar
Sylvain Henry committed
845
         --     See Note [Scoped tyvars in a TcTyCon] in GHC.Core.TyCon
846 847 848 849 850 851
       ; let spec_req_tvs        = map snd scoped_prs
             n_spec              = length spec_req_tvs - tyConArity tc
             (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs
             sorted_spec_tvs     = scopedSort spec_tvs
                 -- NB: We can't do the sort until we've zonked
                 --     Maintain the L-R order of scoped_tvs
852 853 854

       -- Step 2a: find all the Inferred variables we want to quantify over
       ; dvs1 <- candidateQTyVarsOfKinds $
855
                 (tc_res_kind : map tyVarKind spec_req_tvs)
856 857 858 859
       ; let dvs2 = dvs1 `delCandidates` spec_req_tvs

       -- Step 2b: quantify, mainly meaning skolemise the free variables
       -- Returned 'inferred' are scope-sorted and skolemised
860
       ; inferred <- quantifyTyVars dvs2
861

862 863 864 865 866
       ; traceTc "generaliseTcTyCon: pre zonk"
           (vcat [ text "tycon =" <+> ppr tc
                 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
                 , text "tc_res_kind =" <+> ppr tc_res_kind
                 , text "dvs1 =" <+> ppr dvs1
867 868
                 , text "inferred =" <+> pprTyVars inferred ])

869 870 871 872 873 874 875
       -- Step 3: Final zonk (following kind generalisation)
       -- See Note [Swizzling the tyvars before generaliseTcTyCon]
       ; ze <- emptyZonkEnv
       ; (ze, inferred)        <- zonkTyBndrsX ze inferred
       ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
       ; (ze, req_tvs)         <- zonkTyBndrsX ze req_tvs
       ; tc_res_kind           <- zonkTcTypeToTypeX ze tc_res_kind
876

877
       ; traceTc "generaliseTcTyCon: post zonk" $
878
         vcat [ text "tycon =" <+> ppr tc
879 880
              , text "inferred =" <+> pprTyVars inferred
              , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
881 882 883 884 885 886
              , text "sorted_spec_tvs =" <+> pprTyVars sorted_spec_tvs
              , text "req_tvs =" <+> ppr req_tvs
              , text "zonk-env =" <+> ppr ze ]

       -- Step 4: Make the TyConBinders.
       ; let dep_fv_set     = candidateKindVars dvs1
887
             inferred_tcbs  = mkNamedTyConBinders Inferred inferred
888
             specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs
889
             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) req_tvs
890

891
       -- Step 5: Assemble the final list.
892 893 894 895
             final_tcbs = concat [ inferred_tcbs
                                 , specified_tcbs
                                 , required_tcbs ]

896 897 898
       -- Step 6: Make the result TcTyCon
             tycon = mkTcTyCon (tyConName tc) final_tcbs tc_res_kind
                            (mkTyVarNamePairs (sorted_spec_tvs ++ req_tvs))
899 900 901
                            True {- it's generalised now -}
                            (tyConFlavour tc)

902
       ; traceTc "generaliseTcTyCon done" $
903 904
         vcat [ text "tycon =" <+> ppr tc
              , text "tc_res_kind =" <+> ppr tc_res_kind
905
              , text "dep_fv_set =" <+> ppr dep_fv_set
906 907
              , text "inferred_tcbs =" <+> ppr inferred_tcbs
              , text "specified_tcbs =" <+> ppr specified_tcbs
908 909 910
              , text "required_tcbs =" <+> ppr required_tcbs
              , text "final_tcbs =" <+> ppr final_tcbs ]

911
       -- Step 7: Check for validity.
912 913 914
       -- We do this here because we're about to put the tycon into the
       -- the environment, and we don't want anything malformed there
       ; checkTyConTelescope tycon
dreixel's avatar
dreixel committed
915

916
       ; return tycon }
917

918 919 920
{- Note [Required, Specified, and Inferred for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Each forall'd type variable in a type or kind is one of
921

922
  * Required: an argument must be provided at every call site
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
923

924 925
  * Specified: the argument can be inferred at call sites, but
    may be instantiated with visible type/kind application
926

927 928
  * Inferred: the must be inferred at call sites; it
    is unavailable for use with visible type/kind application.
929

930 931 932 933
Why have Inferred at all? Because we just can't make user-facing
promises about the ordering of some variables. These might swizzle
around even between minor released. By forbidding visible type
application, we ensure users aren't caught unawares.
934

Sylvain Henry's avatar
Sylvain Henry committed
935
Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep.
936

937 938 939 940 941 942 943 944 945 946 947 948 949 950 951
The question for this Note is this:
   given a TyClDecl, how are its quantified type variables classified?
Much of the debate is memorialized in #15743.

Here is our design choice. When inferring the ordering of variables
for a TyCl declaration (that is, for those variables that he user
has not specified the order with an explicit `forall`), we use the
following order:

 1. Inferred variables
 2. Specified variables; in the left-to-right order in which
    the user wrote them, modified by scopedSort (see below)
    to put them in depdendency order.
 3. Required variables before a top-level ::
 4. All variables after a top-level ::
Tobias Dammers's avatar
Tobias Dammers committed
952 953 954

If this ordering does not make a valid telescope, we reject the definition.

955 956 957 958
Example:
  data SameKind :: k -> k -> *
  data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

959
For Bad:
960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977
  - a, c, d, x are Required; they are explicitly listed by the user
    as the positional arguments of Bad
  - b is Specified; it appears explicitly in a kind signature
  - k, the kind of a, is Inferred; it is not mentioned explicitly at all

Putting variables in the order Inferred, Specified, Required
gives us this telescope:
  Inferred:  k
  Specified: b : Proxy a
  Required : (a : k) (c : Proxy b) (d : Proxy a) (x : SameKind b d)

But this order is ill-scoped, because b's kind mentions a, which occurs
after b in the telescope. So we reject Bad.

Associated types
~~~~~~~~~~~~~~~~
For associated types everything above is determined by the
associated-type declaration alone, ignoring the class header.
978
Here is an example (#15592)
979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000
  class C (a :: k) b where
    type F (x :: b a)

In the kind of C, 'k' is Specified.  But what about F?
In the kind of F,

 * Should k be Inferred or Specified?  It's Specified for C,
   but not mentioned in F's declaration.

 * In which order should the Specified variables a and b occur?
   It's clearly 'a' then 'b' in C's declaration, but the L-R ordering
   in F's declaration is 'b' then 'a'.

In both cases we make the choice by looking at F's declaration alone,
so it gets the kind
   F :: forall {k}. forall b a. b a -> Type

How it works
~~~~~~~~~~~~
These design choices are implemented by two completely different code
paths for

1001 1002
  * Declarations with a standalone kind signature or a complete user-specified
    kind signature (CUSK). Handled by the kcCheckDeclHeader.
1003

1004 1005
  * Declarations without a kind signature (standalone or CUSK) are handled by
    kcInferDeclHeader; see Note [Inferring kinds for type declarations].
1006 1007

Note that neither code path worries about point (4) above, as this
Tobias Dammers's avatar
Tobias Dammers committed
1008
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
1009 1010 1011 1012 1013 1014 1015 1016 1017
*after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.)

We can tell Inferred apart from Specified by looking at the scoped
tyvars; Specified are always included there.

Design alternatives
~~~~~~~~~~~~~~~~~~~
* For associated types we considered putting the class variables
  before the local variables, in a nod to the treatment for class
1018
  methods. But it got too compilicated; see #15592, comment:21ff.
Tobias Dammers's avatar
Tobias Dammers committed
1019 1020 1021

* We rigidly require the ordering above, even though we could be much more
  permissive. Relevant musings are at
1022
  https://gitlab.haskell.org/ghc/ghc/issues/15743#note_161623
Tobias Dammers's avatar
Tobias Dammers committed
1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034
  The bottom line conclusion is that, if the user wants a different ordering,
  then can specify it themselves, and it is better to be predictable and dumb
  than clever and capricious.

  I (Richard) conjecture we could be fully permissive, allowing all classes
  of variables to intermix. We would have to augment ScopedSort to refuse to
  reorder Required variables (or check that it wouldn't have). But this would
  allow more programs. See #15743 for examples. Interestingly, Idris seems
  to allow this intermixing. The intermixing would be fully specified, in that
  we can be sure that inference wouldn't change between versions. However,
  would users be able to predict it? That I cannot answer.

1035 1036
Test cases (and tickets) relevant to these design decisions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tobias Dammers's avatar
Tobias Dammers committed
1037 1038 1039
  T15591*
  T15592*
  T15743*
1040

1041 1042 1043 1044 1045 1046 1047 1048 1049
Note [Inferring kinds for type declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This note deals with /inference/ for type declarations
that do not have a CUSK.  Consider
  data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x)
  data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y)

We do kind inference as follows:

1050
* Step 1: inferInitialKinds, and in particular kcInferDeclHeader.
1051
  Make a unification variable for each of the Required and Specified
1052
  type variables in the header.
1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071

  Record the connection between the Names the user wrote and the
  fresh unification variables in the tcTyConScopedTyVars field
  of the TcTyCon we are making
      [ (a,  aa)
      , (k1, kk1)
      , (k2, kk2)
      , (x,  xx) ]
  (I'm using the convention that double letter like 'aa' or 'kk'
  mean a unification variable.)

  These unification variables
    - Are TyVarTvs: that is, unification variables that can
      unify only with other type variables.
      See Note [Signature skolems] in TcType

    - Have complete fresh Names; see TcMType
      Note [Unification variables need fresh Names]

1072
  Assign initial monomorphic kinds to S, T
1073 1074
          T :: kk1 -> * -> kk2 -> *
          S :: kk3 -> * -> kk4 -> *
1075

1076
* Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
1077
  T, with these monomorphic kinds.  Now kind-check the declarations,
1078 1079
  and solve the resulting equalities.  The goal here is to discover
  constraints on all these unification variables.
1080 1081 1082 1083 1084 1085

  Here we find that kk1 := kk3, and kk2 := kk4.

  This is why we can't use skolems for kk1 etc; they have to
  unify with each other.

1086
* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
1087 1088 1089 1090 1091
  We find the free variables of the kind, skolemise them,
  sort them out into Inferred/Required/Specified (see the above
  Note [Required, Specified, and Inferred for types]),
  and perform some validity checks.

1092
  This makes the utterly-final TyConBinders for the TyCon.
1093 1094 1095 1096

  All this is very similar at the level of terms: see TcBinds
  Note [Quantified variables in partial type signatures]

1097 1098
  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]

1099 1100 1101
* Step 4.  Extend the type environment with a TcTyCon for S and T, now
  with their utterly-final polymorphic kinds (needed for recursive
  occurrences of S, T).  Now typecheck the declarations, and build the
1102
  final AlgTyCon for S and T resp.
1103

1104 1105
The first three steps are in kcTyClGroup; the fourth is in
tcTyClDecls.
1106 1107 1108 1109 1110 1111 1112

There are some wrinkles

* Do not default TyVarTvs.  We always want to kind-generalise over
  TyVarTvs, and /not/ default them to Type. By definition a TyVarTv is
  not allowed to unify with a type; it must stand for a type
  variable. Hence the check in TcSimplify.defaultTyVarTcS, and
1113
  TcMType.defaultTyVar.  Here's another example (#14555):
1114 1115 1116
     data Exp :: [TYPE rep] -> TYPE rep -> Type where
        Lam :: Exp (a:xs) b -> Exp xs (a -> b)
  We want to kind-generalise over the 'rep' variable.
1117
  #14563 is another example.
1118

1119
* Duplicate type variables. Consider #11203
1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143
    data SameKind :: k -> k -> *
    data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
  Here we will unify k1 with k2, but this time doing so is an error,
  because k1 and k2 are bound in the same declaration.

  We spot this during validity checking (findDupTyVarTvs),
  in generaliseTcTyCon.

* Required arguments.  Even the Required arguments should be made
  into TyVarTvs, not skolems.  Consider
    data T k (a :: k)
  Here, k is a Required, dependent variable. For uniformity, it is helpful
  to have k be a TyVarTv, in parallel with other dependent variables.

* Duplicate skolemisation is expected.  When generalising in Step 3,
  we may find that one of the variables we want to quantify has
  already been skolemised.  For example, suppose we have already
  generalise S. When we come to T we'll find that kk1 (now the same as
  kk3) has already been skolemised.

  That's fine -- but it means that
    a) when collecting quantification candidates, in
       candidateQTyVarsOfKind, we must collect skolems
    b) quantifyTyVars should be a no-op on such a skolem
1144 1145 1146

Note [Tricky scoping in generaliseTcTyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1147
Consider #16342
1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162
  class C (a::ka) x where
    cop :: D a x => x -> Proxy a -> Proxy a
    cop _ x = x :: Proxy (a::ka)

  class D (b::kb) y where
    dop :: C b y => y -> Proxy b -> Proxy b
    dop _ x = x :: Proxy (b::kb)

C and D are mutually recursive, by the time we get to
generaliseTcTyCon we'll have unified kka := kkb.

But when typechecking the default declarations for 'cop' and 'dop' in
tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
But at that point all we have is the utterly-final Class itself.

1163
Conclusion: the classTyVars of a class must have the same Name as
1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187
that originally assigned by the user.  In our example, C must have
classTyVars {a, ka, x} while D has classTyVars {a, kb, y}.  Despite
the fact that kka and kkb got unified!

We achieve this sleight of hand in generaliseTcTyCon, using
the specialised function zonkRecTyVarBndrs.  We make the call
   zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
where the [ka,a,x] are the Names originally assigned by the user, and
[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
   kkb :-> (ka :: <zonked kind of kkb>)
   aa  :-> (a  :: <konked kind of aa>)
   etc
That is, it maps each skolemised TcTyVars to the utterly-final
TyVar to put in the class, with its correct user-specified name.
When generalising D we'll do the same thing, but the ZonkEnv will map
   kkb :-> (kb :: <zonked kind of kkb>)
   bb  :-> (b  :: <konked kind of bb>)
   etc
Note that 'kkb' again appears in the domain of the mapping, but this
time mapped to 'kb'.  That's how C and D end up with differently-named
final TyVars despite the fact that we unified kka:=kkb

zonkRecTyVarBndrs we need to do knot-tying because of the need to
1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220
apply this same substitution to the kind of each.

Note [Inferring visible dependent quantification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data T k :: k -> Type where
    MkT1 :: T Type Int
    MkT2 :: T (Type -> Type) Maybe

This looks like it should work. However, it is polymorphically recursive,
as the uses of T in the constructor types specialize the k in the kind
of T. This trips up our dear users (#17131, #17541), and so we add
a "landmark" context (which cannot be suppressed) whenever we
spot inferred visible dependent quantification (VDQ).

It's hard to know when we've actually been tripped up by polymorphic recursion
specifically, so we just include a note to users whenever we infer VDQ. The
testsuite did not show up a single spurious inclusion of this message.

The context is added in addVDQNote, which looks for a visible TyConBinder
that also appears in the TyCon's kind. (I first looked at the kind for
a visible, dependent quantifier, but Note [No polymorphic recursion] in
TcHsType defeats that approach.) addVDQNote is used in kcTyClDecl,
which is used only when inferring the kind of a tycon (never with a CUSK or
SAK).

Once upon a time, I (Richard E) thought that the tycon-kind could
not be a forall-type. But this is wrong: data T :: forall k. k -> Type
(with -XNoCUSKs) could end up here. And this is all OK.


-}
1221

1222
--------------
1223 1224 1225
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
tcExtendKindEnvWithTyCons tcs
  = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
1226 1227

--------------
1228
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
1229 1230 1231
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
1232
--    See Note [Recursion and promoting data constructors]
1233 1234 1235 1236 1237

mkPromotionErrorEnv decls
  = foldr (plusNameEnv . mk_prom_err_env . unLoc)
          emptyNameEnv decls

1238
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
1239 1240 1241
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
1242 1243
    mkNameEnv [ (familyDeclName at, APromotionErr TyConPE)
              | L _ at <- ats ]
1244

1245
mk_prom_err_env (DataDecl { tcdLName = L _ name
1246 1247 1248 1249
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
1250 1251
              | L _ con' <- cons
              , L _ con  <- getConNames con' ]
1252 1253 1254 1255 1256 1257

mk_prom_err_env decl
  = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
    -- Works for family declarations too

--------------
1258
inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
1259 1260
-- Returns a TcTyCon for each TyCon bound by the decls,
-- each with its initial kind
1261

1262 1263 1264 1265
inferInitialKinds decls
  = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls)
       ; tcs <- concatMapM infer_initial_kind decls
       ; traceTc "inferInitialKinds done }" empty
1266
       ; return tcs }
1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284
  where
    infer_initial_kind = addLocM (getInitialKind InitialKindInfer)

-- Check type/class declarations against their standalone kind signatures or
-- CUSKs, producing a generalized TcTyCon for each.
checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon]
checkInitialKinds decls
  = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls)
       ; tcs <- concatMapM check_initial_kind decls
       ; traceTc "checkInitialKinds done }" empty
       ; return tcs }
  where
    check_initial_kind (ldecl, msig) =
      addLocM (getInitialKind (InitialKindCheck msig)) ldecl

-- | Get the initial kind of a TyClDecl, either generalized or non-generalized,
-- depending on the 'InitialKindStrategy'.
getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon]
1285

dreixel's avatar
dreixel committed
1286
-- Allocate a fresh kind variable for each TyCon and Class
1287
-- For each tycon, return a TcTyCon with kind k
1288
-- where k is the kind of tc, derived from the LHS
1289 1290
--         of the definition (and probably including
--         kind unification variables)
dreixel's avatar
dreixel committed
1291
--      Example: data T a b = ...
1292
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
1293
--
1294 1295 1296 1297
-- This pass deals with (ie incorporates into the kind it produces)
--   * The kind signatures on type-variable binders
--   * The result kinds signature on a TyClDecl
--
1298 1299
-- No family instances are passed to checkInitialKinds/inferInitialKinds
getInitialKind strategy
1300
    (ClassDecl { tcdLName = L _ name
1301 1302
               , tcdTyVars = ktvs
               , tcdATs = ats })
1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317
  = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $
                return (TheKind constraintKind)
       ; let parent_tv_prs = tcTyConScopedTyVars cls
            -- See Note [Don't process associated types in getInitialKind]
       ; inner_tcs <-
           tcExtendNameTyVarEnv parent_tv_prs $
           mapM (addLocM (getAssocFamInitialKind cls)) ats
       ; return (cls : inner_tcs) }
  where
    getAssocFamInitialKind cls =
      case strategy of
        InitialKindInfer -> get_fam_decl_initial_kind (Just cls)
        InitialKindCheck _ -> check_initial_kind_assoc_fam cls

getInitialKind strategy
1318
    (DataDecl { tcdLName = L _ name
1319 1320 1321 1322
              , tcdTyVars = ktvs
              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                         , dd_ND = new_or_data } })
  = do  { let flav = newOrDataToFlavour new_or_data
1323 1324 1325 1326
              ctxt = DataKindCtxt name
        ; tc <- kcDeclHeader strategy name flav ktvs $
                case m_sig of
                  Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
1327
                  Nothing -> return $ dataDeclDefaultResultKind new_or_data
1328 1329
        ; return [tc] }

1330 1331
getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
  = do { tc <- get_fam_decl_initial_kind Nothing decl
1332
       ; return [tc] }
1333

1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350
getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam =
  FamilyDecl { fdLName     = unLoc -> name
             , fdTyVars    = ktvs
             , fdResultSig = unLoc -> resultSig
             , fdInfo      = info } } )
  = do { let flav = getFamFlav Nothing info
             ctxt = TyFamResKindCtxt name
       ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $
               case famResultKindSignature resultSig of
                 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
                 Nothing ->
                   case msig of
                     CUSK -> return (TheKind liftedTypeKind)
                     SAKS _ -> return AnyKind
       ; return [tc] }

getInitialKind strategy
1351
    (SynDecl { tcdLName = L _ name
1352 1353 1354 1355 1356 1357 1358 1359
             , tcdTyVars = ktvs
             , tcdRhs = rhs })
  = do { let ctxt = TySynKindCtxt name
       ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $
               case hsTyKindSig rhs of
                 Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig
                 Nothing -> return AnyKind
       ; return [tc] }
1360

1361
getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec
1362
getInitialKind _ (FamDecl {tcdFam = XFamilyDecl nec}) = noExtCon nec
1363
getInitialKind _ (XTyClDecl nec) = noExtCon nec
1364

1365 1366
get_fam_decl_initial_kind
  :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls
1367 1368
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
1369
get_fam_decl_initial_kind mb_parent_tycon