/
TcTyClsDecls.lhs
1193 lines (1026 loc) · 46 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 AQUA Project, Glasgow University, 1996-1998
%
\section[TcTyClsDecls]{Typecheck type and class declarations}
\begin{code}
module TcTyClsDecls (
tcTyAndClassDecls, tcIdxTyInstDecl
) where
#include "HsVersions.h"
import HsSyn ( TyClDecl(..), HsConDetails(..), HsTyVarBndr(..),
ConDecl(..), Sig(..), NewOrData(..), ResType(..),
tyClDeclTyVars, isSynDecl, isClassDecl, isIdxTyDecl,
isKindSigDecl, hsConArgs, LTyClDecl, tcdName,
hsTyVarName, LHsTyVarBndr, LHsType, HsType(..),
mkHsAppTy
)
import HsTypes ( HsBang(..), getBangStrictness, hsLTyVarNames )
import BasicTypes ( RecFlag(..), StrictnessMark(..) )
import HscTypes ( implicitTyThings, ModDetails )
import BuildTyCl ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
mkDataTyConRhs, mkNewTyConRhs )
import TcRnMonad
import TcEnv ( TyThing(..),
tcLookupLocated, tcLookupLocatedGlobal,
tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
tcExtendRecEnv, tcLookupTyVar, InstInfo )
import TcTyDecls ( calcRecFlags, calcClassCycles, calcSynCycles )
import TcClassDcl ( tcClassSigs, tcAddDeclCtxt )
import TcHsType ( kcHsTyVars, kcHsLiftedSigType, kcHsType,
kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
kcHsSigType, tcHsBangType, tcLHsConResTy,
tcDataKindSig, kcCheckHsType )
import TcMType ( newKindVar, checkValidTheta, checkValidType,
-- checkFreeness,
UserTypeCtxt(..), SourceTyCtxt(..) )
import TcType ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
mkArrowKind, liftedTypeKind, mkTyVarTys,
tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
import Type ( PredType(..), splitTyConApp_maybe, mkTyVarTy,
newTyConInstRhs, isLiftedTypeKind, Kind
-- pprParendType, pprThetaArrow
)
import Generics ( validGenericMethodType, canDoGenerics )
import Class ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
import TyCon ( TyCon, AlgTyConRhs( AbstractTyCon, OpenDataTyCon,
OpenNewTyCon ),
SynTyConRhs( OpenSynTyCon, SynonymTyCon ),
tyConDataCons, mkForeignTyCon, isProductTyCon,
isRecursiveTyCon, isOpenTyCon,
tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName,
isNewTyCon, isDataTyCon, tyConKind,
setTyConArgPoss )
import DataCon ( DataCon, dataConUserType, dataConName,
dataConFieldLabels, dataConTyCon, dataConAllTyVars,
dataConFieldType, dataConResTys )
import Var ( TyVar, idType, idName )
import VarSet ( elemVarSet, mkVarSet )
import Name ( Name, getSrcLoc )
import Outputable
import Maybe ( isJust, fromJust, isNothing, catMaybes )
import Maybes ( expectJust )
import Monad ( unless )
import Unify ( tcMatchTys, tcMatchTyX )
import Util ( zipLazy, isSingleton, notNull, sortLe )
import List ( partition, elemIndex )
import SrcLoc ( Located(..), unLoc, getLoc, srcLocSpan )
import ListSetOps ( equivClasses, minusList )
import Digraph ( SCC(..) )
import DynFlags ( DynFlag( Opt_GlasgowExts, Opt_Generics,
Opt_UnboxStrictFields ) )
\end{code}
%************************************************************************
%* *
\subsection{Type checking for type and class declarations}
%* *
%************************************************************************
Dealing with a group
~~~~~~~~~~~~~~~~~~~~
Consider a mutually-recursive group, binding
a type constructor T and a class C.
Step 1: getInitialKind
Construct a KindEnv by binding T and C to a kind variable
Step 2: kcTyClDecl
In that environment, do a kind check
Step 3: Zonk the kinds
Step 4: buildTyConOrClass
Construct an environment binding T to a TyCon and C to a Class.
a) Their kinds comes from zonking the relevant kind variable
b) Their arity (for synonyms) comes direct from the decl
c) The funcional dependencies come from the decl
d) The rest comes a knot-tied binding of T and C, returned from Step 4
e) The variances of the tycons in the group is calculated from
the knot-tied stuff
Step 5: tcTyClDecl1
In this environment, walk over the decls, constructing the TyCons and Classes.
This uses in a strict way items (a)-(c) above, which is why they must
be constructed in Step 4. Feed the results back to Step 4.
For this step, pass the is-recursive flag as the wimp-out flag
to tcTyClDecl1.
Step 6: Extend environment
We extend the type environment with bindings not only for the TyCons and Classes,
but also for their "implicit Ids" like data constructors and class selectors
Step 7: checkValidTyCl
For a recursive group only, check all the decls again, just
to check all the side conditions on validity. We could not
do this before because we were in a mutually recursive knot.
Identification of recursive TyCons
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
@TyThing@s.
Identifying a TyCon as recursive serves two purposes
1. Avoid infinite types. Non-recursive newtypes are treated as
"transparent", like type synonyms, after the type checker. If we did
this for all newtypes, we'd get infinite types. So we figure out for
each newtype whether it is "recursive", and add a coercion if so. In
effect, we are trying to "cut the loops" by identifying a loop-breaker.
2. Avoid infinite unboxing. This is nothing to do with newtypes.
Suppose we have
data T = MkT Int T
f (MkT x t) = f t
Well, this function diverges, but we don't want the strictness analyser
to diverge. But the strictness analyser will diverge because it looks
deeper and deeper into the structure of T. (I believe there are
examples where the function does something sane, and the strictness
analyser still diverges, but I can't see one now.)
Now, concerning (1), the FC2 branch currently adds a coercion for ALL
newtypes. I did this as an experiment, to try to expose cases in which
the coercions got in the way of optimisations. If it turns out that we
can indeed always use a coercion, then we don't risk recursive types,
and don't need to figure out what the loop breakers are.
For newtype *families* though, we will always have a coercion, so they
are always loop breakers! So you can easily adjust the current
algorithm by simply treating all newtype families as loop breakers (and
indeed type families). I think.
\begin{code}
tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
-> TcM TcGblEnv -- Input env extended by types and classes
-- and their implicit Ids,DataCons
tcTyAndClassDecls boot_details allDecls
= do { -- Omit instances of indexed types; they are handled together
-- with the *heads* of class instances
; let decls = filter (not . isIdxTyDecl . unLoc) allDecls
-- First check for cyclic type synonysm or classes
-- See notes with checkCycleErrs
; checkCycleErrs decls
; mod <- getModule
; traceTc (text "tcTyAndCl" <+> ppr mod)
; (syn_tycons, alg_tyclss) <- fixM (\ ~(rec_syn_tycons, rec_alg_tyclss) ->
do { let { -- Seperate ordinary synonyms from all other type and
-- class declarations and add all associated type
-- declarations from type classes. The latter is
-- required so that the temporary environment for the
-- knot includes all associated family declarations.
; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
decls
; alg_at_decls = concatMap addATs alg_decls
}
-- Extend the global env with the knot-tied results
-- for data types and classes
--
-- We must populate the environment with the loop-tied
-- T's right away, because the kind checker may "fault
-- in" some type constructors that recursively
-- mention T
; let gbl_things = mkGlobalThings alg_at_decls rec_alg_tyclss
; tcExtendRecEnv gbl_things $ do
-- Kind-check the declarations
{ (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls
; let { -- Calculate rec-flag
; calc_rec = calcRecFlags boot_details rec_alg_tyclss
; tc_decl = addLocM (tcTyClDecl calc_rec) }
-- Type-check the type synonyms, and extend the envt
; syn_tycons <- tcSynDecls kc_syn_decls
; tcExtendGlobalEnv syn_tycons $ do
-- Type-check the data types and classes
{ alg_tyclss <- mappM tc_decl kc_alg_decls
; return (syn_tycons, concat alg_tyclss)
}}})
-- Finished with knot-tying now
-- Extend the environment with the finished things
; tcExtendGlobalEnv (syn_tycons ++ alg_tyclss) $ do
-- Perform the validity check
{ traceTc (text "ready for validity check")
; mappM_ (addLocM checkValidTyCl) decls
; traceTc (text "done")
-- Add the implicit things;
-- we want them in the environment because
-- they may be mentioned in interface files
; let { implicit_things = concatMap implicitTyThings alg_tyclss }
; traceTc ((text "Adding" <+> ppr alg_tyclss)
$$ (text "and" <+> ppr implicit_things))
; tcExtendGlobalEnv implicit_things getGblEnv
}}
where
addATs decl@(L _ (ClassDecl {tcdATs = ats})) = decl : ats
addATs decl = [decl]
mkGlobalThings :: [LTyClDecl Name] -- The decls
-> [TyThing] -- Knot-tied, in 1-1 correspondence with the decls
-> [(Name,TyThing)]
-- Driven by the Decls, and treating the TyThings lazily
-- make a TypeEnv for the new things
mkGlobalThings decls things
= map mk_thing (decls `zipLazy` things)
where
mk_thing (L _ (ClassDecl {tcdLName = L _ name}), ~(AClass cl))
= (name, AClass cl)
mk_thing (L _ decl, ~(ATyCon tc))
= (tcdName decl, ATyCon tc)
\end{code}
%************************************************************************
%* *
\subsection{Type checking instances of indexed types}
%* *
%************************************************************************
Instances of indexed types are somewhat of a hybrid. They are processed
together with class instance heads, but can contain data constructors and hence
they share a lot of kinding and type checking code with ordinary algebraic
data types (and GADTs).
\begin{code}
tcIdxTyInstDecl :: LTyClDecl Name
-> TcM (Maybe InstInfo, Maybe TyThing) -- Nothing if error
tcIdxTyInstDecl (L loc decl)
= -- Prime error recovery, set source location
recoverM (returnM (Nothing, Nothing)) $
setSrcSpan loc $
tcAddDeclCtxt decl $
do { -- indexed data types require -fglasgow-exts and can't be in an
-- hs-boot file
; gla_exts <- doptM Opt_GlasgowExts
; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
; checkTc gla_exts $ badIdxTyDecl (tcdLName decl)
; checkTc (not is_boot) $ badBootTyIdxDeclErr
-- perform kind and type checking
; tcIdxTyInstDecl1 decl
}
tcIdxTyInstDecl1 :: TyClDecl Name
-> TcM (Maybe InstInfo, Maybe TyThing) -- Nothing if error
tcIdxTyInstDecl1 (decl@TySynonym {})
= kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
do { -- check that the family declaration is for a synonym
unless (isSynTyCon family) $
addErr (wrongKindOfFamily family)
; -- (1) kind check the right hand side of the type equation
; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
-- (2) type check type equation
; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
; t_typats <- mappM tcHsKindedType k_typats
; t_rhs <- tcHsKindedType k_rhs
-- construct type rewrite rule
-- !!!of the form: forall t_tvs. (tcdLName decl) t_typats = t_rhs
; return (Nothing, Nothing) -- !!!TODO: need InstInfo for eq axioms
}}
tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
tcdCons = cons})
= kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
do { -- check that the family declaration is for the right kind
unless (new_or_data == NewType && isNewTyCon family ||
new_or_data == DataType && isDataTyCon family) $
addErr (wrongKindOfFamily family)
; -- (1) kind check the data declaration as usual
; k_decl <- kcDataDecl decl k_tvs
; let k_ctxt = tcdCtxt k_decl
k_cons = tcdCons k_decl
-- result kind must be '*' (otherwise, we have too few patterns)
; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr tc_name
-- (2) type check indexed data type declaration
; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
; unbox_strict <- doptM Opt_UnboxStrictFields
-- Check that we don't use GADT syntax for indexed types
; checkTc h98_syntax (badGadtIdxTyDecl tc_name)
-- Check that a newtype has exactly one constructor
; checkTc (new_or_data == DataType || isSingleton k_cons) $
newtypeConError tc_name (length k_cons)
; t_typats <- mappM tcHsKindedType k_typats
; stupid_theta <- tcHsKindedContext k_ctxt
; tycon <- fixM (\ tycon -> do
{ data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
tycon t_tvs))
k_cons
; tc_rhs <-
case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType ->
ASSERT( isSingleton data_cons )
mkNewTyConRhs tc_name tycon (head data_cons)
; buildAlgTyCon tc_name t_tvs stupid_theta tc_rhs Recursive
False h98_syntax (Just (family, t_typats))
-- We always assume that indexed types are recursive. Why?
-- (1) Due to their open nature, we can never be sure that a
-- further instance might not introduce a new recursive
-- dependency. (2) They are always valid loop breakers as
-- they involve a coercion.
})
-- construct result
; return (Nothing, Just (ATyCon tycon))
}}
where
h98_syntax = case cons of -- All constructors have same shape
L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
other -> True
-- Kind checking of indexed types
-- -
-- Kind check type patterns and kind annotate the embedded type variables.
--
-- * 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 functions.
--
kcIdxTyPats :: TyClDecl Name
-> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
-- ^^kinded tvs ^^kinded ty pats ^^res kind
-> TcM a
kcIdxTyPats decl thing_inside
= kcHsTyVars (tcdTyVars decl) $ \tvs ->
do { tc_ty_thing <- tcLookupLocated (tcdLName decl)
; let { family = case tc_ty_thing of
AGlobal (ATyCon family) -> family
; (kinds, resKind) = splitKindFunTys (tyConKind family)
; hs_typats = fromJust $ tcdTyPats decl }
-- we may not have more parameters than the kind indicates
; checkTc (length kinds >= length hs_typats) $
tooManyParmsErr (tcdLName decl)
-- type functions can have a higher-kinded result
; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
; typats <- zipWithM kcCheckHsType hs_typats kinds
; thing_inside tvs typats resultKind family
}
where
\end{code}
%************************************************************************
%* *
Kind checking
%* *
%************************************************************************
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.
Indexed Types
~~~~~~~~~~~~~
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 an indexed type 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 indexed types altogether in the following. However, we need to
include the kind signatures of associated types into the construction of the
initial kind environment. (This is handled by `allDecls').
\begin{code}
kcTyClDecls syn_decls alg_decls
= do { -- First extend the kind env with each data type, class, and
-- indexed type, mapping them to a type variable
let initialKindDecls = concat [allDecls decl | L _ decl <- alg_decls]
; alg_kinds <- mappM getInitialKind initialKindDecls
; tcExtendKindEnv alg_kinds $ do
-- Now kind-check the type synonyms, in dependency order
-- We do these 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
{ (kc_syn_decls, syn_kinds) <- kcSynDecls (calcSynCycles syn_decls)
; tcExtendKindEnv syn_kinds $ do
-- Now kind-check the data type, class, and kind signatures,
-- returning kind-annotated decls; we don't kind-check
-- instances of indexed types yet, but leave this to
-- `tcInstDecls1'
{ kc_alg_decls <- mappM (wrapLocM kcTyClDecl)
(filter (not . isIdxTyDecl . unLoc) alg_decls)
; return (kc_syn_decls, kc_alg_decls) }}}
where
-- get all declarations relevant for determining the initial kind
-- environment
allDecls (decl@ClassDecl {tcdATs = ats}) = decl : [ at
| L _ at <- ats
, isKindSigDecl at]
allDecls decl | isIdxTyDecl decl = []
| otherwise = [decl]
------------------------------------------------------------------------
getInitialKind :: TyClDecl Name -> TcM (Name, TcKind)
-- Only for data type, class, and indexed type declarations
-- Get as much info as possible from the data, class, or indexed type decl,
-- so as to maximise usefulness of error messages
getInitialKind decl
= do { arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
; res_kind <- mk_res_kind decl
; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
where
mk_arg_kind (UserTyVar _) = newKindVar
mk_arg_kind (KindedTyVar _ kind) = return kind
mk_res_kind (TyFunction { tcdKind = kind }) = return kind
mk_res_kind (TyData { tcdKindSig = Just kind }) = return kind
-- On GADT-style and data signature declarations we allow a kind
-- signature
-- data T :: *->* where { ... }
mk_res_kind other = return liftedTypeKind
----------------
kcSynDecls :: [SCC (LTyClDecl Name)]
-> TcM ([LTyClDecl Name], -- Kind-annotated decls
[(Name,TcKind)]) -- Kind bindings
kcSynDecls []
= return ([], [])
kcSynDecls (group : groups)
= do { (decl, nk) <- kcSynDecl group
; (decls, nks) <- tcExtendKindEnv [nk] (kcSynDecls groups)
; return (decl:decls, nk:nks) }
----------------
kcSynDecl :: SCC (LTyClDecl Name)
-> TcM (LTyClDecl Name, -- Kind-annotated decls
(Name,TcKind)) -- Kind bindings
kcSynDecl (AcyclicSCC ldecl@(L loc decl))
= tcAddDeclCtxt decl $
kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
do { traceTc (text "kcd1" <+> ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl))
<+> brackets (ppr k_tvs))
; (k_rhs, rhs_kind) <- kcHsType (tcdSynRhs decl)
; traceTc (text "kcd2" <+> ppr (unLoc (tcdLName decl)))
; let tc_kind = foldr (mkArrowKind . kindedTyVarKind) rhs_kind k_tvs
; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
(unLoc (tcdLName decl), tc_kind)) })
kcSynDecl (CyclicSCC decls)
= do { recSynErr decls; failM } -- Fail here to avoid error cascade
-- of out-of-scope tycons
kindedTyVarKind (L _ (KindedTyVar _ k)) = k
------------------------------------------------------------------------
kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
-- Not used for type synonyms (see kcSynDecl)
kcTyClDecl decl@(TyData {})
= ASSERT( not . isJust $ tcdTyPats decl ) -- must not be instance of idx ty
kcTyClDeclBody decl $
kcDataDecl decl
kcTyClDecl decl@(TyFunction {})
= kcTyClDeclBody decl $ \ tvs' ->
return (decl {tcdTyVars = tvs'})
kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
= kcTyClDeclBody decl $ \ tvs' ->
do { is_boot <- tcIsHsBoot
; ctxt' <- kcHsContext ctxt
; ats' <- mappM (wrapLocM kcTyClDecl) ats
; sigs' <- mappM (wrapLocM kc_sig ) sigs
; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs',
tcdATs = ats'}) }
where
kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
; return (TypeSig nm op_ty') }
kc_sig other_sig = return other_sig
kcTyClDecl decl@(ForeignType {})
= return decl
kcTyClDeclBody :: TyClDecl Name
-> ([LHsTyVarBndr Name] -> TcM a)
-> TcM a
-- getInitialKind has made a suitably-shaped kind for the type or class
-- Unpack it, and attribute those kinds to the type variables
-- Extend the env with bindings for the tyvars, taken from
-- the kind of the tycon/class. Give it to the thing inside, and
-- check the result kind matches
kcTyClDeclBody decl thing_inside
= tcAddDeclCtxt decl $
do { tc_ty_thing <- tcLookupLocated (tcdLName decl)
; let tc_kind = case tc_ty_thing of { AThing k -> k }
(kinds, _) = splitKindFunTys tc_kind
hs_tvs = tcdTyVars decl
kinded_tvs = ASSERT( length kinds >= length hs_tvs )
[ L loc (KindedTyVar (hsTyVarName tv) k)
| (L loc tv, k) <- zip hs_tvs kinds]
; tcExtendKindEnvTvs kinded_tvs (thing_inside kinded_tvs) }
-- Kind check a data declaration, assuming that we already extended the
-- kind environment with the type variables of the left-hand side (these
-- kinded type variables are also passed as the second parameter).
--
kcDataDecl :: TyClDecl Name -> [LHsTyVarBndr Name] -> TcM (TyClDecl Name)
kcDataDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
tvs
= do { ctxt' <- kcHsContext ctxt
; cons' <- mappM (wrapLocM kc_con_decl) cons
; return (decl {tcdTyVars = tvs, tcdCtxt = ctxt', tcdCons = cons'}) }
where
kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res) = do
kcHsTyVars ex_tvs $ \ex_tvs' -> do
ex_ctxt' <- kcHsContext ex_ctxt
details' <- kc_con_details details
res' <- case res of
ResTyH98 -> return ResTyH98
ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
return (ConDecl name expl ex_tvs' ex_ctxt' details' res')
kc_con_details (PrefixCon btys)
= do { btys' <- mappM kc_larg_ty btys ; return (PrefixCon btys') }
kc_con_details (InfixCon bty1 bty2)
= do { bty1' <- kc_larg_ty bty1; bty2' <- kc_larg_ty bty2; return (InfixCon bty1' bty2') }
kc_con_details (RecCon fields)
= do { fields' <- mappM kc_field fields; return (RecCon fields') }
kc_field (fld, bty) = do { bty' <- kc_larg_ty bty ; return (fld, bty') }
kc_larg_ty bty = case new_or_data of
DataType -> kcHsSigType bty
NewType -> kcHsLiftedSigType bty
-- Can't allow an unlifted type for newtypes, because we're effectively
-- going to remove the constructor while coercing it to a lifted type.
-- And newtypes can't be bang'd
\end{code}
%************************************************************************
%* *
\subsection{Type checking}
%* *
%************************************************************************
\begin{code}
tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
tcSynDecls [] = return []
tcSynDecls (decl : decls)
= do { syn_tc <- addLocM tcSynDecl decl
; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
; return (syn_tc : syn_tcs) }
tcSynDecl
(TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
= tcTyVarBndrs tvs $ \ tvs' -> do
{ traceTc (text "tcd1" <+> ppr tc_name)
; rhs_ty' <- tcHsKindedType rhs_ty
; return (ATyCon (buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty'))) }
--------------------
tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
tcTyClDecl calc_isrec decl
= tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
-- kind signature for a type function
tcTyClDecl1 _calc_isrec
(TyFunction {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = kind})
= tcTyVarBndrs tvs $ \ tvs' -> do
{ traceTc (text "type family: " <+> ppr tc_name)
; gla_exts <- doptM Opt_GlasgowExts
-- Check that we don't use kind signatures without Glasgow extensions
; checkTc gla_exts $ badSigTyDecl tc_name
; return [ATyCon $ buildSynTyCon tc_name tvs' (OpenSynTyCon kind)]
}
-- kind signature for an indexed data type
tcTyClDecl1 _calc_isrec
(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
tcdLName = L _ tc_name, tcdKindSig = Just ksig, tcdCons = []})
= tcTyVarBndrs tvs $ \ tvs' -> do
{ traceTc (text "data/newtype family: " <+> ppr tc_name)
; extra_tvs <- tcDataKindSig (Just ksig)
; let final_tvs = tvs' ++ extra_tvs -- we may not need these
; checkTc (null . unLoc $ ctxt) $ badKindSigCtxt tc_name
; gla_exts <- doptM Opt_GlasgowExts
-- Check that we don't use kind signatures without Glasgow extensions
; checkTc gla_exts $ badSigTyDecl tc_name
; tycon <- buildAlgTyCon tc_name final_tvs []
(case new_or_data of
DataType -> OpenDataTyCon
NewType -> OpenNewTyCon)
Recursive False True Nothing
; return [ATyCon tycon]
}
tcTyClDecl1 calc_isrec
(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
= tcTyVarBndrs tvs $ \ tvs' -> do
{ extra_tvs <- tcDataKindSig mb_ksig
; let final_tvs = tvs' ++ extra_tvs
; stupid_theta <- tcHsKindedContext ctxt
; want_generic <- doptM Opt_Generics
; unbox_strict <- doptM Opt_UnboxStrictFields
; gla_exts <- doptM Opt_GlasgowExts
; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
-- Check that we don't use GADT syntax in H98 world
; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
-- Check that we don't use kind signatures without Glasgow extensions
; checkTc (gla_exts || isNothing mb_ksig) (badSigTyDecl 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 there's at least one condecl,
-- or else we're reading an hs-boot file, or -fglasgow-exts
; checkTc (not (null cons) || gla_exts || is_boot)
(emptyConDeclsErr tc_name)
-- Check that a newtype has exactly one constructor
; checkTc (new_or_data == DataType || isSingleton cons)
(newtypeConError tc_name (length cons))
; tycon <- fixM (\ tycon -> do
{ data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
tycon final_tvs))
cons
; tc_rhs <-
if null cons && is_boot -- In a hs-boot file, empty cons means
then return AbstractTyCon -- "don't know"; hence Abstract
else case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType ->
ASSERT( isSingleton data_cons )
mkNewTyConRhs tc_name tycon (head data_cons)
; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
(want_generic && canDoGenerics data_cons) h98_syntax Nothing
})
; return [ATyCon tycon]
}
where
is_rec = calc_isrec tc_name
h98_syntax = case cons of -- All constructors have same shape
L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
other -> True
tcTyClDecl1 calc_isrec
(ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs,
tcdCtxt = ctxt, tcdMeths = meths,
tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
= tcTyVarBndrs tvs $ \ tvs' -> do
{ ctxt' <- tcHsKindedContext ctxt
; fds' <- mappM (addLocM tc_fundep) fundeps
; atss <- mappM (addLocM (tcTyClDecl1 (const Recursive))) ats
; let ats' = zipWith setTyThingPoss atss (map (tcdTyVars . unLoc) ats)
; sig_stuff <- tcClassSigs class_name sigs meths
; clas <- fixM (\ clas ->
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 = calc_isrec tycon_name
in
buildClass class_name tvs' ctxt' fds' ats'
sig_stuff tc_isrec)
; return (AClass clas : 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' <- mappM tcLookupTyVar tvs1 ;
; tvs2' <- mappM tcLookupTyVar tvs2 ;
; return (tvs1', tvs2') }
-- For each AT argument compute the position of the corresponding class
-- parameter in the class head. This will later serve as a permutation
-- vector when checking the validity of instance declarations.
setTyThingPoss [ATyCon tycon] atTyVars =
let classTyVars = hsLTyVarNames tvs
poss = catMaybes
. map (`elemIndex` classTyVars)
. hsLTyVarNames
$ atTyVars
-- There will be no Nothing, as we already passed renaming
in
ATyCon (setTyConArgPoss tycon poss)
setTyThingPoss _ _ = panic "TcTyClsDecls.setTyThingPoss"
tcTyClDecl1 calc_isrec
(ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
= returnM [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
-----------------------------------
tcConDecl :: Bool -- True <=> -funbox-strict_fields
-> NewOrData
-> TyCon -> [TyVar]
-> ConDecl Name
-> TcM DataCon
tcConDecl unbox_strict NewType tycon tc_tvs -- Newtypes
(ConDecl name _ ex_tvs ex_ctxt details ResTyH98)
= do { let tc_datacon field_lbls arg_ty
= do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
; buildDataCon (unLoc name) False {- Prefix -}
[NotMarkedStrict]
(map unLoc field_lbls)
tc_tvs [] -- No existentials
[] [] -- No equalities, predicates
[arg_ty']
tycon }
-- Check that a newtype has no existential stuff
; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
; case details of
PrefixCon [arg_ty] -> tc_datacon [] arg_ty
RecCon [(field_lbl, arg_ty)] -> tc_datacon [field_lbl] arg_ty
other ->
failWithTc (newtypeFieldErr name (length (hsConArgs details)))
-- Check that the constructor has exactly one field
}
tcConDecl unbox_strict DataType tycon tc_tvs -- Data types
(ConDecl name _ tvs ctxt details res_ty)
= tcTyVarBndrs tvs $ \ tvs' -> do
{ ctxt' <- tcHsKindedContext ctxt
; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
; let
tc_datacon is_infix field_lbls btys
= do { let bangs = map getBangStrictness btys
; arg_tys <- mappM tcHsBangType btys
; buildDataCon (unLoc name) is_infix
(argStrictness unbox_strict tycon bangs arg_tys)
(map unLoc field_lbls)
univ_tvs ex_tvs eq_preds ctxt' arg_tys
data_tc }
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
-- that way checkValidDataCon can complain if it's wrong.
; case details of
PrefixCon btys -> tc_datacon False [] btys
InfixCon bty1 bty2 -> tc_datacon True [] [bty1,bty2]
RecCon fields -> tc_datacon False field_names btys
where
(field_names, btys) = unzip fields
}
tcResultType :: TyCon
-> [TyVar] -- data T a b c = ...
-> [TyVar] -- where MkT :: forall a b c. ...
-> ResType Name
-> TcM ([TyVar], -- Universal
[TyVar], -- Existential
[(TyVar,Type)], -- Equality predicates
TyCon) -- TyCon given in the ResTy
-- We don't check that the TyCon given in the ResTy is
-- the same as the parent tycon, becuase we are in the middle
-- of a recursive knot; so it's postponed until checkValidDataCon
tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
= return (tc_tvs, dc_tvs, [], decl_tycon)
-- In H98 syntax the dc_tvs are the existential ones
-- data T a b c = forall d e. MkT ...
-- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
-- E.g. data T a b c where
-- MkT :: forall x y z. T (x,y) z z
-- Then we generate
-- ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
= do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
-- NB: tc_tvs and dc_tvs are distinct
; let univ_tvs = choose_univs [] tc_tvs res_tys
-- Each univ_tv is either a dc_tv or a tc_tv
ex_tvs = dc_tvs `minusList` univ_tvs
eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys,
tv `elem` tc_tvs]
; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
where
-- choose_univs uses the res_ty itself if it's a type variable
-- and hasn't already been used; otherwise it uses one of the tc_tvs
choose_univs used tc_tvs []
= ASSERT( null tc_tvs ) []
choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys)
| Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
= tv : choose_univs (tv:used) tc_tvs res_tys
| otherwise
= tc_tv : choose_univs used tc_tvs res_tys
-------------------
argStrictness :: Bool -- True <=> -funbox-strict_fields
-> TyCon -> [HsBang]
-> [TcType] -> [StrictnessMark]
argStrictness unbox_strict tycon bangs arg_tys
= ASSERT( length bangs == length arg_tys )
zipWith (chooseBoxingStrategy unbox_strict tycon) arg_tys bangs
-- We attempt to unbox/unpack a strict field when either:
-- (i) The field is marked '!!', or
-- (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
--
-- We have turned off unboxing of newtypes because coercions make unboxing
-- and reboxing more complicated
chooseBoxingStrategy :: Bool -> TyCon -> TcType -> HsBang -> StrictnessMark
chooseBoxingStrategy unbox_strict_fields tycon arg_ty bang
= case bang of
HsNoBang -> NotMarkedStrict
HsStrict | unbox_strict_fields
&& can_unbox arg_ty -> MarkedUnboxed
HsUnbox | can_unbox arg_ty -> MarkedUnboxed
other -> MarkedStrict
where
-- we can unbox if the type is a chain of newtypes with a product tycon
-- at the end
can_unbox arg_ty = case splitTyConApp_maybe arg_ty of
Nothing -> False
Just (arg_tycon, tycon_args) ->
not (isRecursiveTyCon tycon) &&
isProductTyCon arg_tycon &&
(if isNewTyCon arg_tycon then
can_unbox (newTyConInstRhs arg_tycon tycon_args)
else True)
\end{code}
%************************************************************************
%* *
\subsection{Dependency analysis}
%* *
%************************************************************************
Validity checking is done once the mutually-recursive knot has been
tied, so we can look at things freely.
\begin{code}
checkCycleErrs :: [LTyClDecl Name] -> TcM ()
checkCycleErrs tyclss
| null cls_cycles
= return ()
| otherwise
= do { mappM_ recClsErr cls_cycles
; failM } -- Give up now, because later checkValidTyCl
-- will loop if the synonym is recursive
where
cls_cycles = calcClassCycles tyclss
checkValidTyCl :: TyClDecl Name -> TcM ()
-- We do the validity check over declarations, rather than TyThings
-- only so that we can add a nice context with tcAddDeclCtxt
checkValidTyCl decl
= tcAddDeclCtxt decl $
do { thing <- tcLookupLocatedGlobal (tcdLName decl)
; traceTc (text "Validity of" <+> ppr thing)
; case thing of
ATyCon tc -> checkValidTyCon tc
AClass cl -> checkValidClass cl
; traceTc (text "Done validity of" <+> ppr thing)
}
-------------------------
-- For data types declared with record syntax, we require
-- that each constructor that has a field 'f'
-- (a) has the same result type
-- (b) has the same type for 'f'
-- module alpha conversion of the quantified type variables
-- of the constructor.
checkValidTyCon :: TyCon -> TcM ()
checkValidTyCon tc
| isSynTyCon tc
= case synTyConRhs tc of
OpenSynTyCon _ -> return ()
SynonymTyCon ty -> checkValidType syn_ctxt ty
| otherwise
= -- Check the context on the data decl
checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc) `thenM_`
-- Check arg types of data constructors
mappM_ (checkValidDataCon tc) data_cons `thenM_`
-- Check that fields with the same name share a type
mappM_ check_fields groups
where
syn_ctxt = TySynCtxt name
name = tyConName tc
data_cons = tyConDataCons tc
groups = equivClasses cmp_fld (concatMap get_fields data_cons)
cmp_fld (f1,_) (f2,_) = f1 `compare` f2
get_fields con = dataConFieldLabels con `zip` repeat con
-- dataConFieldLabels may return the empty list, which is fine
-- See Note [GADT record selectors] in MkId.lhs
-- We must check (a) that the named field has the same
-- type in each constructor
-- (b) that those constructors have the same result type
--
-- However, the constructors may have differently named type variable
-- and (worse) we don't know how the correspond to each other. E.g.
-- C1 :: forall a b. { f :: a, g :: b } -> T a b
-- C2 :: forall d c. { f :: c, g :: c } -> T c d
--
-- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
-- result type against other candidates' types BOTH WAYS ROUND.
-- If they magically agrees, take the substitution and
-- apply them to the latter ones, and see if they match perfectly.
check_fields fields@((label, con1) : other_fields)
-- These fields all have the same name, but are from
-- different constructors in the data type
= recoverM (return ()) $ mapM_ checkOne other_fields
-- Check that all the fields in the group have the same type
-- NB: this check assumes that all the constructors of a given
-- data type use the same type variables
where
tvs1 = mkVarSet (dataConAllTyVars con1)
res1 = dataConResTys con1
fty1 = dataConFieldType con1 label
checkOne (_, con2) -- Do it bothways to ensure they are structurally identical
= do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
where
tvs2 = mkVarSet (dataConAllTyVars con2)
res2 = dataConResTys con2
fty2 = dataConFieldType con2 label
checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
= do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
where
mb_subst1 = tcMatchTys tvs1 res1 res2
mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2