mirrored from https://gitlab.haskell.org/ghc/ghc.git
-
Notifications
You must be signed in to change notification settings - Fork 705
/
TcTyClsDecls.lhs
1890 lines (1614 loc) · 79.6 KB
/
TcTyClsDecls.lhs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
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
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
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
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
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
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%
% (c) The University of Glasgow 2006
% (c) The AQUA Project, Glasgow University, 1996-1998
%
TcTyClsDecls: Typecheck type and class declarations
\begin{code}
{-# LANGUAGE TupleSections #-}
module TcTyClsDecls (
tcTyAndClassDecls, tcAddImplicits,
-- Functions used by TcInstDcls to check
-- data/type family instance declarations
kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
tcSynFamInstDecl, tcFamTyPats,
tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
wrongKindOfFamily,
) where
#include "HsVersions.h"
import HsSyn
import HscTypes
import BuildTyCl
import TcRnMonad
import TcEnv
import TcValidity
import TcHsSyn
import TcBinds( tcRecSelBinds )
import FunDeps( growThetaTyVars )
import TcTyDecls
import TcClassDcl
import TcHsType
import TcMType
import TcType
import TysWiredIn( unitTy )
import FamInstEnv
import FamInst
import Coercion( mkCoAxBranch )
import Type
import Kind
import Class
import CoAxiom( CoAxBranch(..) )
import TyCon
import DataCon
import Id
import MkCore ( rEC_SEL_ERROR_ID )
import IdInfo
import Var
import VarEnv
import VarSet
import Module
import Name
import NameSet
import NameEnv
import Outputable
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
import FastString
import Unique ( mkBuiltinUnique )
import BasicTypes
import Bag
import Control.Monad
import Data.List
\end{code}
%************************************************************************
%* *
\subsection{Type checking for type and class declarations}
%* *
%************************************************************************
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
forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
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 *.
\begin{code}
tcTyAndClassDecls :: ModDetails
-> [TyClGroup Name] -- Mutually-recursive groups in dependency order
-> TcM TcGblEnv -- Input env extended by types and classes
-- and their implicit Ids,DataCons
-- Fails if there are any errors
tcTyAndClassDecls boot_details tyclds_s
= checkNoErrs $ -- The code recovers internally, but if anything gave rise to
-- an error we'd better stop now, to avoid a cascade
fold_env tyclds_s -- Type check each group in dependency order folding the global env
where
fold_env :: [TyClGroup Name] -> TcM TcGblEnv
fold_env [] = getGblEnv
fold_env (tyclds:tyclds_s)
= do { tcg_env <- tcTyClGroup boot_details tyclds
; setGblEnv tcg_env $ fold_env tyclds_s }
-- remaining groups are typecheck in the extended global env
tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
-- Typecheck one strongly-connected component of type and class decls
tcTyClGroup boot_details tyclds
= do { -- Step 1: kind-check this group and returns the final
-- (possibly-polymorphic) kind of each TyCon and Class
-- See Note [Kind checking for type and class decls]
names_w_poly_kinds <- kcTyClGroup tyclds
; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
-- Step 2: type-check all groups together, returning
-- the final TyCons and Classes
; tyclss <- fixM $ \ rec_tyclss -> do
{ let rec_flags = calcRecFlags boot_details rec_tyclss
-- Populate environment with knot-tied ATyCon for TyCons
-- NB: if the decls mention any ill-staged data cons
-- (see Note [Recusion and promoting data constructors]
-- we will have failed already in kcTyClGroup, so no worries here
; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
-- Also extend the local type envt with bindings giving
-- the (polymorphic) kind of each knot-tied TyCon or Class
-- See Note [Type checking recursive type and class declarations]
tcExtendKindEnv names_w_poly_kinds $
-- Kind and type check declarations for this group
concatMapM (tcTyClDecl rec_flags) tyclds }
-- Step 3: Perform the validity chebck
-- We can do this now because we are done with the recursive knot
-- Do it before Step 4 (adding implicit things) because the latter
-- expects well-formed TyCons
; tcExtendGlobalEnv tyclss $ do
{ traceTc "Starting validity check" (ppr tyclss)
; checkNoErrs $
mapM_ (recoverM (return ()) . addLocM checkValidTyCl) tyclds
-- We recover, which allows us to report multiple validity errors
-- but we then fail if any are wrong. Lacking the checkNoErrs
-- we get Trac #7175
-- Step 4: Add the implicit things;
-- we want them in the environment because
-- they may be mentioned in interface files
; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
tcAddImplicits tyclss } }
tcAddImplicits :: [TyThing] -> TcM TcGblEnv
tcAddImplicits tyclss
= tcExtendGlobalEnvImplicit implicit_things $
tcRecSelBinds rec_sel_binds
where
implicit_things = concatMap implicitTyThings tyclss
rec_sel_binds = mkRecSelBinds tyclss
zipRecTyClss :: [(Name, Kind)]
-> [TyThing] -- Knot-tied
-> [(Name,TyThing)]
-- Build a name-TyThing mapping for the things bound by decls
-- being careful not to look at the [TyThing]
-- The TyThings in the result list must have a visible ATyCon,
-- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
zipRecTyClss kind_pairs rec_things
= [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
where
rec_type_env :: TypeEnv
rec_type_env = mkTypeEnv rec_things
get name = case lookupTypeEnv rec_type_env name of
Just (ATyCon tc) -> tc
other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
\end{code}
%************************************************************************
%* *
Kind checking
%* *
%************************************************************************
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:
1. Make up a kind variable for each parameter of the *data* type,
and class, decls, and extend the kind environment (which is in
the TcLclEnv)
2. Dependency-analyse the type *synonyms* (which must be non-recursive),
and kind-check them in dependency order. Extend the kind envt.
3. Kind check the data type and class decls
Synonyms are treated differently to data type and classes,
because a type synonym can be an unboxed type
type Foo = Int#
and a kind variable can't unify with UnboxedTypeKind
So we infer their kinds in dependency order
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables. For example:
class C a where
op :: D b => a -> b -> b
class D c where
bop :: (Monad c) => ...
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.
However type synonyms work differently. They can have kinds which don't
just involve (->) and *:
type R = Int# -- Kind #
type S a = Array# a -- Kind * -> #
type T a b = (# a,b #) -- Kind * -> * -> (# a,b #)
So we must infer their kinds from their right-hand sides *first* and then
use them, whereas for the mutually recursive data types D we bring into
scope kind bindings D -> k, where k is a kind variable, and do inference.
Type families
~~~~~~~~~~~~~
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.
The kind of a type family is solely determinded by its kind signature;
hence, only kind signatures participate in the construction of the initial
kind environment (as constructed by `getInitialKind'). In fact, we ignore
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').
\begin{code}
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
-- Kind check this group, kind generalize, and return the resulting local env
-- This bindds the TyCons and Classes of the group, but not the DataCons
-- See Note [Kind checking for type and class decls]
kcTyClGroup decls
= do { mod <- getModule
; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
-- Kind checking;
-- 1. Bind kind variables for non-synonyms
-- 2. Kind-check synonyms, and bind kinds of those synonyms
-- 3. Kind-check non-synonyms
-- 4. Generalise the inferred kinds
-- See Note [Kind checking for type and class decls]
-- Step 1: Bind kind variables for non-synonyms
; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
; initial_kinds <- getInitialKinds TopLevel non_syn_decls
; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
-- Step 2: Set initial envt, kind-check the synonyms
; lcl_env <- tcExtendTcTyThingEnv initial_kinds $
kcSynDecls (calcSynCycles syn_decls)
-- Step 3: Set extended envt, kind-check the non-synonyms
; setLclEnv lcl_env $
mapM_ kcLTyClDecl non_syn_decls
-- Step 4: generalisation
-- Kind checking done for this group
-- Now we have to kind generalize the flexis
; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
; traceTc "kcTyClGroup result" (ppr res)
; return res }
where
generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
-- For polymorphic things this is a no-op
generalise kind_env name
= do { let kc_kind = case lookupNameEnv kind_env name of
Just (AThing k) -> k
_ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
; kvs <- kindGeneralize (tyVarsOfType kc_kind)
; kc_kind' <- zonkTcKind kc_kind -- Make sure kc_kind' has the final,
-- skolemised kind variables
; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
; return (name, mkForAllTys kvs kc_kind') }
generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
generaliseTCD kind_env (L _ decl)
| ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
= do { first <- generalise kind_env name
; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
; return (first : rest) }
| FamDecl { tcdFam = fam } <- decl
= do { res <- generaliseFamDecl kind_env fam
; return [res] }
| ForeignType {} <- decl
= pprPanic "generaliseTCD" (ppr decl)
| otherwise
-- Note: tcdTyVars is safe here because we've eliminated FamDecl and ForeignType
= do { res <- generalise kind_env (tcdName decl)
; return [res] }
generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
= generalise kind_env name
mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
mk_thing_env [] = []
mk_thing_env (decl : decls)
| L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
= (nm, APromotionErr ClassPE) :
(map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
(mk_thing_env decls)
| otherwise
= (tcdName (unLoc decl), APromotionErr TyConPE) :
(mk_thing_env decls)
getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
getInitialKinds top_lvl decls
= tcExtendTcTyThingEnv (mk_thing_env decls) $
concatMapM (addLocM (getInitialKind top_lvl)) decls
getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return (tc, AThing k)
-- where k is the kind of tc, derived from the LHS
-- of the definition (and probably including
-- kind unification variables)
-- Example: data T a b = ...
-- return (T, kv1 -> kv2 -> kv3)
--
-- 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
--
-- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
-- Note [ARecDataCon: Recursion and promoting data constructors]
--
-- No family instances are passed to getInitialKinds
getInitialKind top_lvl (FamDecl { tcdFam = decl }) = getFamDeclInitialKind top_lvl decl
getInitialKind _ (ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { inner_prs <- getFamDeclInitialKinds ats
; let main_pr = (name, AThing (mkArrowKinds arg_kinds constraintKind))
; return (main_pr : inner_prs) }
getInitialKind _top_lvl decl@(SynDecl {}) = pprPanic "getInitialKind" (ppr decl)
getInitialKind top_lvl (DataDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdDataDefn = defn })
| HsDataDefn { dd_kindSig = Just ksig, dd_cons = cons } <- defn
= ASSERT( isTopLevel top_lvl )
kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
do { res_k <- tcLHsKind ksig
; let body_kind = mkArrowKinds arg_kinds res_k
kvs = varSetElems (tyVarsOfType body_kind)
main_pr = (name, AThing (mkForAllTys kvs body_kind))
inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
-- See Note [Recusion and promoting data constructors]
; return (main_pr : inner_prs) }
| HsDataDefn { dd_cons = cons } <- defn
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { let main_pr = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
inner_prs = [ (unLoc (con_name con), APromotionErr RecDataConPE)
| L _ con <- cons ]
-- See Note [Recusion and promoting data constructors]
; return (main_pr : inner_prs) }
getInitialKind _ (ForeignType { tcdLName = L _ name })
= return [(name, AThing liftedTypeKind)]
getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
= tcExtendTcTyThingEnv [ (n, APromotionErr TyConPE)
| L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
concatMapM (addLocM (getFamDeclInitialKind NotTopLevel)) decls
getFamDeclInitialKind :: TopLevelFlag
-> FamilyDecl Name
-> TcM [(Name, TcTyThing)]
getFamDeclInitialKind top_lvl (FamilyDecl { fdLName = L _ name
, fdTyVars = ktvs
, fdKindSig = ksig })
| isTopLevel top_lvl
= kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
do { res_k <- case ksig of
Just k -> tcLHsKind k
Nothing -> return liftedTypeKind
; let body_kind = mkArrowKinds arg_kinds res_k
kvs = varSetElems (tyVarsOfType body_kind)
; return [ (name, AThing (mkForAllTys kvs body_kind)) ] }
| otherwise
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { res_k <- case ksig of
Just k -> tcLHsKind k
Nothing -> newMetaKindVar
; return [ (name, AThing (mkArrowKinds arg_kinds res_k)) ] }
----------------
kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
kcSynDecls (group : groups)
= do { nk <- kcSynDecl1 group
; tcExtendKindEnv [nk] (kcSynDecls groups) }
kcSynDecl1 :: SCC (LTyClDecl Name)
-> TcM (Name,TcKind) -- Kind bindings
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls) = do { recSynErr decls; failM }
-- Fail here to avoid error cascade
-- of out-of-scope tycons
kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
, tcdRhs = rhs })
-- Returns a possibly-unzonked kind
= tcAddDeclCtxt decl $
kcHsTyVarBndrs False hs_tvs $ \ ks ->
do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)
<+> brackets (ppr ks))
; (_, rhs_kind) <- tcLHsType rhs
; traceTc "kcd2" (ppr name)
; let tc_kind = mkArrowKinds ks rhs_kind
; return (name, tc_kind) }
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
------------------------------------------------------------------------
kcLTyClDecl :: LTyClDecl Name -> TcM ()
-- See Note [Kind checking for type and class decls]
kcLTyClDecl (L loc decl)
= setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl
kcTyClDecl :: TyClDecl Name -> TcM ()
-- This function is used solely for its side effect on kind variables
-- NB kind signatures on the type variables and
-- result kind signature have aready been dealt with
-- by getInitialKind, so we can ignore them here.
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
| HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
= mapM_ (wrapLocM kcConDecl) cons
-- hs_tvs and td_kindSig already dealt with in getInitialKind
-- Ignore the dd_ctxt; heavily deprecated and inconvenient
| HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
= kcTyClTyVars name hs_tvs $
do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM kcConDecl) cons }
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
, tcdCtxt = ctxt, tcdSigs = sigs })
= kcTyClTyVars name hs_tvs $
do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM kc_sig) sigs }
where
kc_sig (TypeSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
kc_sig _ = return ()
kcTyClDecl (ForeignType {}) = return ()
kcTyClDecl (FamDecl {}) = return ()
-------------------
kcConDecl :: ConDecl Name -> TcM ()
kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
, con_cxt = ex_ctxt, con_details = details, con_res = res })
= addErrCtxt (dataConCtxt name) $
kcHsTyVarBndrs False ex_tvs $ \ _ ->
do { _ <- tcHsContext ex_ctxt
; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
; _ <- tcConRes res
; return () }
\end{code}
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't want to allow promotion in a strongly connected component
when kind checking.
Consider:
data T f = K (f (K Any))
When kind checking the `data T' declaration the local env contains the
mappings:
T -> AThing <some initial kind>
K -> ARecDataCon
ANothing is only used for DataCons, and only used during type checking
in tcTyClGroup.
%************************************************************************
%* *
\subsection{Type checking}
%* *
%************************************************************************
Note [Type checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this point we have completed *kind-checking* of a mutually
recursive group of type/class decls (done in kcTyClGroup). However,
we discarded the kind-checked types (eg RHSs of data type decls);
note that kcTyClDecl returns (). There are two reasons:
* It's convenient, because we don't have to rebuild a
kinded HsDecl (a fairly elaborate type)
* It's necessary, because after kind-generalisation, the
TyCons/Classes may now be kind-polymorphic, and hence need
to be given kind arguments.
Example:
data T f a = MkT (f a) (T f a)
During kind-checking, we give T the kind T :: k1 -> k2 -> *
and figure out constraints on k1, k2 etc. Then we generalise
to get T :: forall k. (k->*) -> k -> *
So now the (T f a) in the RHS must be elaborated to (T k f a).
However, during tcTyClDecl of T (above) we will be in a recursive
"knot". So we aren't allowed to look at the TyCon T itself; we are only
allowed to put it (lazily) in the returned structures. But when
kind-checking the RHS of T's decl, we *do* need to know T's kind (so
that we can correctly elaboarate (T k f a). How can we get T's kind
without looking at T? Delicate answer: during tcTyClDecl, we extend
*Global* env with T -> ATyCon (the (not yet built) TyCon for T)
*Local* env with T -> AThing (polymorphic kind of T)
Then:
* During TcHsType.kcTyVar we look in the *local* env, to get the
known kind for T.
* But in TcHsType.ds_type (and ds_var_app in particular) we look in
the *global* env to get the TyCon. But we must be careful not to
force the TyCon or we'll get a loop.
This fancy footwork (with two bindings for T) is only necesary for the
TyCons or Classes of this recursive group. Earlier, finished groups,
live in the global env only.
\begin{code}
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
tcTyClDecl rec_info (L loc decl)
= setSrcSpan loc $ tcAddDeclCtxt decl $
traceTc "tcTyAndCl-x" (ppr decl) >>
tcTyClDecl1 NoParentTyCon rec_info decl
-- "type family" declarations
tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
= tcFamDecl1 parent fd
-- "type" synonym declaration
tcTyClDecl1 _parent _rec_info
(SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
= ASSERT( isNoParent _parent )
tcTyClTyVars tc_name tvs $ \ tvs' kind ->
tcTySynRhs tc_name tvs' kind rhs
-- "data/newtype" declaration
tcTyClDecl1 _parent rec_info
(DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
= ASSERT( isNoParent _parent )
tcTyClTyVars tc_name tvs $ \ tvs' kind ->
tcDataDefn rec_info tc_name tvs' kind defn
tcTyClDecl1 _parent rec_info
(ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
, tcdCtxt = ctxt, tcdMeths = meths
, tcdFDs = fundeps, tcdSigs = sigs
, tcdATs = ats, tcdATDefs = at_defs })
= ASSERT( isNoParent _parent )
do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
tcTyClTyVars class_name tvs $ \ tvs' kind ->
do { MASSERT( isConstraintKind kind )
; let -- This little knot is just so we can get
-- hold of the name of the class TyCon, which we
-- need to look up its recursiveness
tycon_name = tyConName (classTyCon clas)
tc_isrec = rti_is_rec rec_info tycon_name
; ctxt' <- tcHsContext ctxt
; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
-- Squeeze out any kind unification variables
; fds' <- mapM (addLocM tc_fundep) fundeps
; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
; clas <- buildClass False {- Must include unfoldings for selectors -}
class_name tvs' ctxt' fds' at_stuff
sig_stuff tc_isrec
; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
; return (clas, tvs', gen_dm_env) }
; let { gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
| (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
, let gen_dm_tau = expectJust "tcTyClDecl1" $
lookupNameEnv gen_dm_env (idName sel_id)
, let gen_dm_ty = mkSigmaTy tvs'
[mkClassPred clas (mkTyVarTys tvs')]
gen_dm_tau
]
; class_ats = map ATyCon (classATs clas) }
; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
-- NB: Order is important due to the call to `mkGlobalThings' when
-- tying the the type and class declaration type checking knot.
where
tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
; tvs2' <- mapM tc_fd_tyvar tvs2 ;
; return (tvs1', tvs2') }
tc_fd_tyvar name -- Scoped kind variables are bound to unification variables
-- which are now fixed, so we can zonk
= do { tv <- tcLookupTyVar name
; ty <- zonkTyVarOcc emptyZonkEnv tv
-- Squeeze out any kind unification variables
; case getTyVar_maybe ty of
Just tv' -> return tv'
Nothing -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
tcTyClDecl1 _ _
(ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
= return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
\end{code}
\begin{code}
tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
tcFamDecl1 parent
(FamilyDecl {fdFlavour = TypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
= tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
{ traceTc "type family:" (ppr tc_name)
; checkFamFlag tc_name
; let syn_rhs = SynFamilyTyCon { synf_open = True, synf_injective = False }
; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent
; return [ATyCon tycon] }
tcFamDecl1 parent
(FamilyDecl {fdFlavour = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
= tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
{ traceTc "data family:" (ppr tc_name)
; checkFamFlag tc_name
; extra_tvs <- tcDataKindSig kind
; let final_tvs = tvs' ++ extra_tvs -- we may not need these
tycon = buildAlgTyCon tc_name final_tvs Nothing []
DataFamilyTyCon Recursive
False -- Not promotable to the kind level
True -- GADT syntax
parent
; return [ATyCon tycon] }
tcTySynRhs :: Name
-> [TyVar] -> Kind
-> LHsType Name -> TcM [TyThing]
tcTySynRhs tc_name tvs kind hs_ty
= do { env <- getLclEnv
; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
; rhs_ty <- tcCheckLHsType hs_ty kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; tycon <- buildSynTyCon tc_name tvs (SynonymTyCon rhs_ty)
kind NoParentTyCon
; return [ATyCon tycon] }
tcDataDefn :: RecTyInfo -> Name
-> [TyVar] -> Kind
-> HsDataDefn Name -> TcM [TyThing]
-- NB: not used for newtype/data instances (whether associated or not)
tcDataDefn rec_info tc_name tvs kind
(HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_kindSig = mb_ksig
, dd_cons = cons })
= do { extra_tvs <- tcDataKindSig kind
; let final_tvs = tvs ++ extra_tvs
; stupid_theta <- tcHsContext ctxt
; kind_signatures <- xoptM Opt_KindSignatures
; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
-- Check that we don't use kind signatures without Glasgow extensions
; case mb_ksig of
Nothing -> return ()
Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
; tc_kind <- tcLHsKind hs_k
; checkKind kind tc_kind
; return () }
; h98_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
; tycon <- fixM $ \ tycon -> do
{ let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
; tc_rhs <-
if null cons && is_boot -- In a hs-boot file, empty cons means
then return totallyAbstractTyConRhs -- "don't know"; hence totally Abstract
else case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs tc_name tycon (head data_cons)
; return (buildAlgTyCon tc_name final_tvs cType stupid_theta tc_rhs
(rti_is_rec rec_info tc_name)
(rti_promotable rec_info)
(not h98_syntax) NoParentTyCon) }
; return [ATyCon tycon] }
\end{code}
%************************************************************************
%* *
Typechecking associated types (in class decls)
(including the associated-type defaults)
%* *
%************************************************************************
Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The following is an example of associated type defaults:
class C a where
data D a
type F a b :: *
type F a Z = [a] -- Default
type F a (S n) = F a n -- Default
Note that:
- We can have more than one default definition for a single associated type,
as long as they do not overlap (same rules as for instances)
- We can get default definitions only for type families, not data families
\begin{code}
tcClassATs :: Name -- The class name (not knot-tied)
-> TyConParent -- The class parent of this associated type
-> [LFamilyDecl Name] -- Associated types.
-> [LTyFamInstDecl Name] -- Associated type defaults.
-> TcM [ClassATItem]
tcClassATs class_name parent ats at_defs
= do { -- Complain about associated type defaults for non associated-types
sequence_ [ failWithTc (badATErr class_name n)
| n <- map (tyFamInstDeclName . unLoc) at_defs
, not (n `elemNameSet` at_names) ]
; mapM tc_at ats }
where
at_names = mkNameSet (map (unLoc . fdLName . unLoc) ats)
at_defs_map :: NameEnv [LTyFamInstDecl Name]
-- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
(tyFamInstDeclName (unLoc at_def)) [at_def])
emptyNameEnv at_defs
tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
; let at_defs = lookupNameEnv at_defs_map (unLoc $ fdLName $ unLoc at)
`orElse` []
; atd <- concatMapM (tcDefaultAssocDecl fam_tc) at_defs
; return (fam_tc, atd) }
-------------------------
tcDefaultAssocDecl :: TyCon -- ^ Family TyCon
-> LTyFamInstDecl Name -- ^ RHS
-> TcM [CoAxBranch] -- ^ Type checked RHS and free TyVars
tcDefaultAssocDecl fam_tc (L loc decl)
= setSrcSpan loc $
tcAddTyFamInstCtxt decl $
do { traceTc "tcDefaultAssocDecl" (ppr decl)
; (_space, branches) <- tcSynFamInstDecl fam_tc decl
; ASSERT( case _space of { NoFamInstSpace -> True ; _ -> False } )
return branches }
-- We check for well-formedness and validity later, in checkValidClass
-------------------------
-- returns an optional type space specifier along with the branches
tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name
-> TcM (FamInstSpace, [CoAxBranch])
-- Placed here because type family instances appear as
-- default decls in class declarations
tcSynFamInstDecl fam_tc (TyFamInstSingle { tfid_eqn = eqn })
= do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
; eqn' <- tcTyFamInstEqn fam_tc eqn
; return (NoFamInstSpace, [eqn']) }
tcSynFamInstDecl fam_tc (TyFamInstBranched { tfid_eqns = eqns
, tfid_space = mspace })
-- we know the first equation matches the fam_tc because of the lookup logic
-- now, just check that all other names match the first
= do { tcSynFamInstNames first names
; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
; space' <- check_space mspace
; eqns' <- mapM (tcTyFamInstEqn fam_tc) eqns
; return (space', eqns') }
where
names = map (tfie_tycon . unLoc) eqns
first = head names
check_space :: Maybe (LTyFamInstSpace Name) -> TcM FamInstSpace
check_space Nothing = return NoFamInstSpace
check_space (Just (L loc (TyFamInstSpace { tfis_tycon = tycon
, tfis_pats = pats })))
= setSrcSpan loc $
tcAddTyFamInstSpaceCtxt $
do { checkTc (tycon == first) (badTypeSpace tycon first)
; tcFamTyPats fam_tc pats Nothing $
\tvs pats' _kind -> mkFamInstSpace loc tvs pats' }
-- Checks to make sure that all the names in an instance group are the same
tcSynFamInstNames :: Located Name -> [Located Name] -> TcM ()
tcSynFamInstNames (L _ first) names
= do { let badNames = filter ((/= first) . unLoc) names
; mapM_ (failLocated (wrongNamesInInstGroup first)) badNames }
where
failLocated :: (Name -> SDoc) -> Located Name -> TcM ()
failLocated msg_fun (L loc name)
= setSrcSpan loc $
failWithTc (msg_fun name)
tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
tcTyFamInstEqn fam_tc
(L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
= setSrcSpan loc $
tcFamTyPats fam_tc pats (Just $ discardResult . (tcCheckLHsType hs_ty)) $
\tvs' pats' res_kind ->
do { rhs_ty <- tcCheckLHsType hs_ty res_kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
-- Used for 'data instance' only
-- Ordinary 'data' is handled by kcTyClDec
kcDataDefn (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
= do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM kcConDecl) cons
; kcResultKind mb_kind res_k }
------------------
kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
kcResultKind Nothing res_k
= checkKind res_k liftedTypeKind
-- type family F a
-- defaults to type family F a :: *
kcResultKind (Just k) res_k
= do { k' <- tcLHsKind k
; checkKind k' res_k }
-------------------------
-- Kind check type patterns and kind annotate the embedded type variables.
-- type instance F [a] = rhs
--
-- * Here we check that a type instance matches its kind signature, but we do
-- not check whether there is a pattern for each type index; the latter
-- check is only required for type synonym instances.
-----------------
tcFamTyPats :: TyCon
-> HsWithBndrs [LHsType Name] -- Patterns
-> Maybe (TcKind -> TcM ()) -- Kind checker for RHS
-- result is ignored
-> ([TKVar] -> [TcType] -> Kind -> TcM a)
-> TcM a
-- Check the type patterns of a type or data family instance
-- type instance F <pat1> <pat2> = <type>
-- The 'tyvars' are the free type variables of pats
--
-- NB: The family instance declaration may be an associated one,
-- nested inside an instance decl, thus
-- instance C [a] where
-- type F [a] = ...
-- In that case, the type variable 'a' will *already be in scope*
-- (and, if C is poly-kinded, so will its kind parameter).
tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
mb_kind_checker thing_inside
= do { -- A family instance must have exactly the same number of type
-- parameters as the family declaration. You can't write
-- type family F a :: * -> *
-- type instance F Int y = y
-- because then the type (F Int) would be like (\y.y)
; let (fam_kvs, fam_body) = splitForAllTys (tyConKind fam_tc)
fam_arity = tyConArity fam_tc - length fam_kvs
; checkTc (length arg_pats == fam_arity) $
wrongNumberOfParmsErr fam_arity
-- Instantiate with meta kind vars
; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
; loc <- getSrcSpanM
; let (arg_kinds, res_kind)
= splitKindFunTysN fam_arity $
substKiWith fam_kvs fam_arg_kinds fam_body
hs_tvs = HsQTvs { hsq_kvs = kvars
, hsq_tvs = userHsTyVarBndrs loc tvars }
-- Kind-check and quantify
-- See Note [Quantifying over family patterns]
; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
do { maybe_do mb_kind_checker res_kind
; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
; let all_args = fam_arg_kinds ++ typats
-- Find free variables (after zonking) and turn
-- them into skolems, so that we don't subsequently
-- replace a meta kind var with AnyK
-- Very like kindGeneralize
; qtkvs <- quantifyTyVars emptyVarSet (tyVarsOfTypes all_args)
-- Zonk the patterns etc into the Type world
; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
; all_args' <- zonkTcTypeToTypes ze all_args
; res_kind' <- zonkTcTypeToType ze res_kind
; traceTc "tcFamTyPats" (pprTvBndrs qtkvs' $$ ppr all_args' $$ ppr res_kind')
; tcExtendTyVarEnv qtkvs' $
thing_inside qtkvs' all_args' res_kind' }
where maybe_do :: Monad m => Maybe (a -> m ()) -> a -> m ()
maybe_do Nothing _ = return ()
maybe_do (Just f) a = f a
\end{code}
Note [Quantifying over family patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to quantify over two different lots of kind variables:
First, the ones that come from the kinds of the tyvar args of
tcTyVarBndrsKindGen, as usual
data family Dist a
-- Proxy :: forall k. k -> *
data instance Dist (Proxy a) = DP
-- Generates data DistProxy = DP
-- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
-- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
Second, the ones that come from the kind argument of the type family
which we pick up using the (tyVarsOfTypes typats) in the result of
the thing_inside of tcHsTyvarBndrsGen.
-- Any :: forall k. k
data instance Dist Any = DA
-- Generates data DistAny k = DA
-- ax7 k :: Dist k (Any k) ~ DistAny k
-- The 'k' comes from kindGeneralizeKinds (Any k)
Note [Quantified kind variables of a family pattern]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider type family KindFam (p :: k1) (q :: k1)
data T :: Maybe k1 -> k2 -> *
type instance KindFam (a :: Maybe k) b = T a b -> Int
The HsBSig for the family patterns will be ([k], [a])
Then in the family instance we want to
* Bring into scope [ "k" -> k:BOX, "a" -> a:k ]
* Kind-check the RHS
* Quantify the type instance over k and k', as well as a,b, thus
type instance [k, k', a:Maybe k, b:k']
KindFam (Maybe k) k' a b = T k k' a b -> Int
Notice that in the third step we quantify over all the visibly-mentioned
type variables (a,b), but also over the implicitly mentioned kind varaibles
(k, k'). In this case one is bound explicitly but often there will be
none. The role of the kind signature (a :: Maybe k) is to add a constraint
that 'a' must have that kind, and to bring 'k' into scope.
%************************************************************************
%* *
Data types
%* *
%************************************************************************
\begin{code}
dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM Bool
dataDeclChecks tc_name new_or_data stupid_theta cons
= do { -- Check that we don't use GADT syntax in H98 world
gadtSyntax_ok <- xoptM Opt_GADTSyntax
; let h98_syntax = consUseH98Syntax cons
; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
-- Check that the stupid theta is empty for a GADT-style declaration
; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
-- Check that a newtype has exactly one constructor
-- Do this before checking for empty data decls, so that
-- we don't suggest -XEmptyDataDecls for newtypes
; checkTc (new_or_data == DataType || isSingleton cons)