1{-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-}
2{-# Language OverloadedStrings #-}
3{-# Language Safe #-}
4module Cryptol.TypeCheck.Error where
5
6import qualified Data.IntMap as IntMap
7import qualified Data.Set as Set
8import Control.DeepSeq(NFData)
9import GHC.Generics(Generic)
10import Data.List((\\),sortBy,groupBy,partition)
11import Data.Function(on)
12
13import qualified Cryptol.Parser.AST as P
14import Cryptol.Parser.Position(Located(..), Range(..))
15import Cryptol.TypeCheck.PP
16import Cryptol.TypeCheck.Type
17import Cryptol.TypeCheck.InferTypes
18import Cryptol.TypeCheck.Subst
19import Cryptol.ModuleSystem.Name(Name)
20import Cryptol.Utils.Ident(Ident)
21import Cryptol.Utils.RecordMap
22
23cleanupErrors :: [(Range,Error)] -> [(Range,Error)]
24cleanupErrors = dropErrorsFromSameLoc
25              . sortBy (compare `on` (cmpR . fst))    -- order errors
26              . dropSubsumed []
27  where
28
29  -- pick shortest error from each location.
30  dropErrorsFromSameLoc = concatMap chooseBestError
31                        . groupBy ((==)    `on` fst)
32
33  addErrorRating (r,e) = (errorImportance e, (r,e))
34  chooseBestError    = map snd
35                     . head
36                     . groupBy ((==) `on` fst)
37                     . sortBy (flip compare `on` fst)
38                     . map addErrorRating
39
40
41  cmpR r  = ( source r    -- First by file
42            , from r      -- Then starting position
43            , to r        -- Finally end position
44            )
45
46  dropSubsumed survived xs =
47    case xs of
48      err : rest ->
49         let keep e = not (subsumes err e)
50         in dropSubsumed (err : filter keep survived) (filter keep rest)
51      [] -> survived
52
53-- | Should the first error suppress the next one.
54subsumes :: (Range,Error) -> (Range,Error) -> Bool
55subsumes (_,NotForAll _ x _) (_,NotForAll _ y _) = x == y
56subsumes (r1,KindMismatch {}) (r2,err) =
57  case err of
58    KindMismatch {} -> r1 == r2
59    _               -> True
60subsumes _ _ = False
61
62data Warning  = DefaultingKind (P.TParam Name) P.Kind
63              | DefaultingWildType P.Kind
64              | DefaultingTo !TVarInfo Type
65                deriving (Show, Generic, NFData)
66
67-- | Various errors that might happen during type checking/inference
68data Error    = KindMismatch (Maybe TypeSource) Kind Kind
69                -- ^ Expected kind, inferred kind
70
71              | TooManyTypeParams Int Kind
72                -- ^ Number of extra parameters, kind of result
73                -- (which should not be of the form @_ -> _@)
74
75              | TyVarWithParams
76                -- ^ A type variable was applied to some arguments.
77
78              | TooManyTySynParams Name Int
79                -- ^ Type-synonym, number of extra params
80
81              | TooFewTyParams Name Int
82                -- ^ Who is missing params, number of missing params
83
84              | RecursiveTypeDecls [Name]
85                -- ^ The type synonym declarations are recursive
86
87              | TypeMismatch TypeSource Type Type
88                -- ^ Expected type, inferred type
89
90              | RecursiveType TypeSource Type Type
91                -- ^ Unification results in a recursive type
92
93              | UnsolvedGoals [Goal]
94                -- ^ A constraint that we could not solve, usually because
95                -- there are some left-over variables that we could not infer.
96
97              | UnsolvableGoals [Goal]
98                -- ^ A constraint that we could not solve and we know
99                -- it is impossible to do it.
100
101              | UnsolvedDelayedCt DelayedCt
102                -- ^ A constraint (with context) that we could not solve
103
104              | UnexpectedTypeWildCard
105                -- ^ Type wild cards are not allowed in this context
106                -- (e.g., definitions of type synonyms).
107
108              | TypeVariableEscaped TypeSource Type [TParam]
109                -- ^ Unification variable depends on quantified variables
110                -- that are not in scope.
111
112              | NotForAll TypeSource TVar Type
113                -- ^ Quantified type variables (of kind *) need to
114                -- match the given type, so it does not work for all types.
115
116              | TooManyPositionalTypeParams
117                -- ^ Too many positional type arguments, in an explicit
118                -- type instantiation
119
120              | BadParameterKind TParam Kind
121                -- ^ Kind other than `*` or `#` given to parameter of
122                --   type synonym, newtype, function signature, etc.
123
124              | CannotMixPositionalAndNamedTypeParams
125
126              | UndefinedTypeParameter (Located Ident)
127
128              | RepeatedTypeParameter Ident [Range]
129
130              | AmbiguousSize TVarInfo (Maybe Type)
131                -- ^ Could not determine the value of a numeric type variable,
132                --   but we know it must be at least as large as the given type
133                --   (or unconstrained, if Nothing).
134
135              | BareTypeApp
136                -- ^ Bare expression of the form `{_}
137
138              | UndefinedExistVar Name
139              | TypeShadowing String Name String
140              | MissingModTParam (Located Ident)
141              | MissingModVParam (Located Ident)
142                deriving (Show, Generic, NFData)
143
144-- | When we have multiple errors on the same location, we show only the
145-- ones with the has highest rating according to this function.
146errorImportance :: Error -> Int
147errorImportance err =
148  case err of
149    BareTypeApp                                      -> 11 -- basically a parse error
150    KindMismatch {}                                  -> 10
151    TyVarWithParams {}                               -> 9
152    TypeMismatch {}                                  -> 8
153    RecursiveType {}                                 -> 7
154    NotForAll {}                                     -> 6
155    TypeVariableEscaped {}                           -> 5
156
157    UndefinedExistVar {}                             -> 10
158    TypeShadowing {}                                 -> 2
159    MissingModTParam {}                              -> 10
160    MissingModVParam {}                              -> 10
161
162    BadParameterKind{}                               -> 9
163    CannotMixPositionalAndNamedTypeParams {}         -> 8
164    TooManyTypeParams {}                             -> 8
165    TooFewTyParams {}                                -> 8
166    TooManyPositionalTypeParams {}                   -> 8
167    UndefinedTypeParameter {}                        -> 8
168    RepeatedTypeParameter {}                         -> 8
169
170    TooManyTySynParams {}                            -> 8
171    UnexpectedTypeWildCard {}                        -> 8
172
173    RecursiveTypeDecls {}                            -> 9
174
175    UnsolvableGoals g
176      | any tHasErrors (map goal g)                  -> 0
177      | otherwise                                    -> 4
178
179    UnsolvedGoals g
180      | any tHasErrors (map goal g)                  -> 0
181      | otherwise                                    -> 4
182
183    UnsolvedDelayedCt dt
184      | any tHasErrors (map goal (dctGoals dt))      -> 0
185      | otherwise                                    -> 3
186
187    AmbiguousSize {}                                 -> 2
188
189
190
191
192instance TVars Warning where
193  apSubst su warn =
194    case warn of
195      DefaultingKind {}     -> warn
196      DefaultingWildType {} -> warn
197      DefaultingTo d ty     -> DefaultingTo d $! (apSubst su ty)
198
199instance FVS Warning where
200  fvs warn =
201    case warn of
202      DefaultingKind {}     -> Set.empty
203      DefaultingWildType {} -> Set.empty
204      DefaultingTo _ ty     -> fvs ty
205
206instance TVars Error where
207  apSubst su err =
208    case err of
209      KindMismatch {}           -> err
210      TooManyTypeParams {}      -> err
211      TyVarWithParams           -> err
212      TooManyTySynParams {}     -> err
213      TooFewTyParams {}         -> err
214      RecursiveTypeDecls {}     -> err
215      TypeMismatch src t1 t2    -> TypeMismatch src !$ (apSubst su t1) !$ (apSubst su t2)
216      RecursiveType src t1 t2   -> RecursiveType src !$ (apSubst su t1) !$ (apSubst su t2)
217      UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs
218      UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs
219      UnsolvedDelayedCt g       -> UnsolvedDelayedCt !$ (apSubst su g)
220      UnexpectedTypeWildCard    -> err
221      TypeVariableEscaped src t xs ->
222                                 TypeVariableEscaped src !$ (apSubst su t) .$ xs
223      NotForAll src x t         -> NotForAll src x !$ (apSubst su t)
224      TooManyPositionalTypeParams -> err
225      CannotMixPositionalAndNamedTypeParams -> err
226
227      BadParameterKind{} -> err
228      UndefinedTypeParameter {} -> err
229      RepeatedTypeParameter {} -> err
230      AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t)
231
232      BareTypeApp -> err
233
234      UndefinedExistVar {} -> err
235      TypeShadowing {}     -> err
236      MissingModTParam {}  -> err
237      MissingModVParam {}  -> err
238
239
240instance FVS Error where
241  fvs err =
242    case err of
243      KindMismatch {}           -> Set.empty
244      TooManyTypeParams {}      -> Set.empty
245      TyVarWithParams           -> Set.empty
246      TooManyTySynParams {}     -> Set.empty
247      TooFewTyParams {}         -> Set.empty
248      RecursiveTypeDecls {}     -> Set.empty
249      TypeMismatch _ t1 t2      -> fvs (t1,t2)
250      RecursiveType _ t1 t2     -> fvs (t1,t2)
251      UnsolvedGoals gs          -> fvs gs
252      UnsolvableGoals gs        -> fvs gs
253      UnsolvedDelayedCt g       -> fvs g
254      UnexpectedTypeWildCard    -> Set.empty
255      TypeVariableEscaped _ t xs-> fvs t `Set.union`
256                                            Set.fromList (map TVBound xs)
257      NotForAll _ x t             -> Set.insert x (fvs t)
258      TooManyPositionalTypeParams -> Set.empty
259      CannotMixPositionalAndNamedTypeParams -> Set.empty
260      UndefinedTypeParameter {}             -> Set.empty
261      RepeatedTypeParameter {}              -> Set.empty
262      AmbiguousSize _ t -> fvs t
263      BadParameterKind tp _ -> Set.singleton (TVBound tp)
264
265      BareTypeApp -> Set.empty
266
267      UndefinedExistVar {} -> Set.empty
268      TypeShadowing {}     -> Set.empty
269      MissingModTParam {}  -> Set.empty
270      MissingModVParam {}  -> Set.empty
271
272instance PP Warning where
273  ppPrec = ppWithNamesPrec IntMap.empty
274
275instance PP Error where
276  ppPrec = ppWithNamesPrec IntMap.empty
277
278
279instance PP (WithNames Warning) where
280  ppPrec _ (WithNames warn names) =
281    addTVarsDescsAfter names warn $
282    case warn of
283      DefaultingKind x k ->
284        text "Assuming " <+> pp x <+> text "to have" <+> P.cppKind k
285
286      DefaultingWildType k ->
287        text "Assuming _ to have" <+> P.cppKind k
288
289      DefaultingTo d ty ->
290        text "Defaulting" <+> pp (tvarDesc d) <+> text "to"
291                                              <+> ppWithNames names ty
292
293instance PP (WithNames Error) where
294  ppPrec _ (WithNames err names) =
295    case err of
296
297      RecursiveType src t1 t2 ->
298        addTVarsDescsAfter names err $
299        nested "Matching would result in an infinite type." $
300          vcat [ "The type: " <+> ppWithNames names t1
301               , "occurs in:" <+> ppWithNames names t2
302               , "When checking" <+> pp src
303               ]
304
305      UnexpectedTypeWildCard ->
306        addTVarsDescsAfter names err $
307        nested "Wild card types are not allowed in this context"
308          "(e.g., they cannot be used in type synonyms)."
309
310      KindMismatch mbsrc k1 k2 ->
311        addTVarsDescsAfter names err $
312        nested "Incorrect type form." $
313         vcat [ "Expected:" <+> cppKind k1
314              , "Inferred:" <+> cppKind k2
315              , kindMismatchHint k1 k2
316              , maybe empty (\src -> "When checking" <+> pp src) mbsrc
317              ]
318
319      TooManyTypeParams extra k ->
320        addTVarsDescsAfter names err $
321        nested "Malformed type."
322          ("Kind" <+> quotes (pp k) <+> "is not a function," $$
323           "but it was applied to" <+> pl extra "parameter" <.> ".")
324
325      TyVarWithParams ->
326        addTVarsDescsAfter names err $
327        nested "Malformed type."
328               "Type variables cannot be applied to parameters."
329
330      TooManyTySynParams t extra ->
331        addTVarsDescsAfter names err $
332        nested "Malformed type."
333          ("Type synonym" <+> nm t <+> "was applied to" <+>
334            pl extra "extra parameters" <.> text ".")
335
336      TooFewTyParams t few ->
337        addTVarsDescsAfter names err $
338        nested "Malformed type."
339          ("Type" <+> nm t <+> "is missing" <+> int few <+> text "parameters.")
340
341      RecursiveTypeDecls ts ->
342        addTVarsDescsAfter names err $
343        nested "Recursive type declarations:"
344               (fsep $ punctuate comma $ map nm ts)
345
346      TypeMismatch src t1 t2 ->
347        addTVarsDescsAfter names err $
348        nested "Type mismatch:" $
349        vcat [ "Expected type:" <+> ppWithNames names t1
350             , "Inferred type:" <+> ppWithNames names t2
351             , mismatchHint t1 t2
352             , "When checking" <+> pp src
353             ]
354
355      UnsolvableGoals gs -> explainUnsolvable names gs
356
357      UnsolvedGoals gs
358        | noUni ->
359          addTVarsDescsAfter names err $
360          nested "Unsolved constraints:" $
361          bullets (map (ppWithNames names) gs)
362
363        | otherwise ->
364          addTVarsDescsBefore names err $
365          nested "subject to the following constraints:" $
366          bullets (map (ppWithNames names) gs)
367
368      UnsolvedDelayedCt g
369        | noUni ->
370          addTVarsDescsAfter names err $
371          nested "Failed to validate user-specified signature." $
372          ppWithNames names g
373        | otherwise ->
374          addTVarsDescsBefore names err $
375          nested "while validating user-specified signature" $
376          ppWithNames names g
377
378      TypeVariableEscaped src t xs ->
379        addTVarsDescsAfter names err $
380        nested ("The type" <+> ppWithNames names t <+>
381                                        "is not sufficiently polymorphic.") $
382          vcat [ "It cannot depend on quantified variables:" <+>
383                          sep (punctuate comma (map (ppWithNames names) xs))
384               , "When checking" <+> pp src
385               ]
386
387      NotForAll src x t ->
388        addTVarsDescsAfter names err $
389        nested "Inferred type is not sufficiently polymorphic." $
390          vcat [ "Quantified variable:" <+> ppWithNames names x
391               , "cannot match type:"   <+> ppWithNames names t
392               , "When checking" <+> pp src
393               ]
394
395      BadParameterKind tp k ->
396        addTVarsDescsAfter names err $
397        vcat [ "Illegal kind assigned to type variable:" <+> ppWithNames names tp
398             , "Unexpected:" <+> pp k
399             ]
400
401      TooManyPositionalTypeParams ->
402        addTVarsDescsAfter names err $
403        "Too many positional type-parameters in explicit type application."
404
405      CannotMixPositionalAndNamedTypeParams ->
406        addTVarsDescsAfter names err $
407        "Named and positional type applications may not be mixed."
408
409      UndefinedTypeParameter x ->
410        addTVarsDescsAfter names err $
411        "Undefined type parameter `" <.> pp (thing x) <.> "`."
412          $$ "See" <+> pp (srcRange x)
413
414      RepeatedTypeParameter x rs ->
415        addTVarsDescsAfter names err $
416        "Multiple definitions for type parameter `" <.> pp x <.> "`:"
417          $$ nest 2 (bullets (map pp rs))
418
419      AmbiguousSize x t ->
420        let sizeMsg =
421               case t of
422                 Just t' -> "Must be at least:" <+> ppWithNames names t'
423                 Nothing -> empty
424         in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg)
425
426      BareTypeApp ->
427        "Unexpected bare type application." $$
428        "Perhaps you meant `( ... ) instead."
429
430      UndefinedExistVar x -> "Undefined type" <+> quotes (pp x)
431      TypeShadowing this new that ->
432        "Type" <+> text this <+> quotes (pp new) <+>
433        "shadowing an existing" <+> text that <+> "with the same name."
434      MissingModTParam x ->
435        "Missing definition for type parameter" <+> quotes (pp (thing x))
436      MissingModVParam x ->
437        "Missing definition for value parameter" <+> quotes (pp (thing x))
438
439
440
441
442    where
443    bullets xs = vcat [ "•" <+> d | d <- xs ]
444
445    nested x y = x $$ nest 2 y
446
447    pl 1 x     = text "1" <+> text x
448    pl n x     = text (show n) <+> text x <.> text "s"
449
450    nm x       = text "`" <.> pp x <.> text "`"
451
452    kindMismatchHint k1 k2 =
453      case (k1,k2) of
454        (KType,KProp) -> "Possibly due to a missing `=>`"
455        _ -> empty
456
457    mismatchHint (TRec fs1) (TRec fs2) =
458      hint "Missing" missing $$ hint "Unexpected" extra
459      where
460        missing = displayOrder fs1 \\ displayOrder fs2
461        extra   = displayOrder fs2 \\ displayOrder fs1
462        hint _ []  = mempty
463        hint s [x] = text s <+> text "field" <+> pp x
464        hint s xs  = text s <+> text "fields" <+> commaSep (map pp xs)
465    mismatchHint _ _ = mempty
466
467    noUni = Set.null (Set.filter isFreeTV (fvs err))
468
469
470
471explainUnsolvable :: NameMap -> [Goal] -> Doc
472explainUnsolvable names gs =
473  addTVarsDescsAfter names gs (bullets (map explain gs))
474
475  where
476  bullets xs = vcat [ "•" <+> d | d <- xs ]
477
478
479
480  explain g =
481    let useCtr = "Unsolvable constraint:" $$
482                  nest 2 (ppWithNames names g)
483
484    in
485    case tNoUser (goal g) of
486      TCon (PC pc) ts ->
487        let tys = [ backticks (ppWithNames names t) | t <- ts ]
488            doc1 : _ = tys
489            custom msg = msg $$
490                         nest 2 (text "arising from" $$
491                                 pp (goalSource g)   $$
492                                 text "at" <+> pp (goalRange g))
493        in
494        case pc of
495          PEqual      -> useCtr
496          PNeq        -> useCtr
497          PGeq        -> useCtr
498          PFin        -> useCtr
499          PPrime      -> useCtr
500
501          PHas sel ->
502            custom ("Type" <+> doc1 <+> "does not have field" <+> f
503                    <+> "of type" <+> (tys !! 1))
504            where f = case sel of
505                        P.TupleSel n _ -> int n
506                        P.RecordSel fl _ -> backticks (pp fl)
507                        P.ListSel n _ -> int n
508
509          PZero  ->
510            custom ("Type" <+> doc1 <+> "does not have `zero`")
511
512          PLogic ->
513            custom ("Type" <+> doc1 <+> "does not support logical operations.")
514
515          PRing ->
516            custom ("Type" <+> doc1 <+> "does not support ring operations.")
517
518          PIntegral ->
519            custom (doc1 <+> "is not an integral type.")
520
521          PField ->
522            custom ("Type" <+> doc1 <+> "does not support field operations.")
523
524          PRound ->
525            custom ("Type" <+> doc1 <+> "does not support rounding operations.")
526
527          PEq ->
528            custom ("Type" <+> doc1 <+> "does not support equality.")
529
530          PCmp        ->
531            custom ("Type" <+> doc1 <+> "does not support comparisons.")
532
533          PSignedCmp  ->
534            custom ("Type" <+> doc1 <+> "does not support signed comparisons.")
535
536          PLiteral ->
537            let doc2 = tys !! 1
538            in custom (doc1 <+> "is not a valid literal of type" <+> doc2)
539
540          PLiteralLessThan ->
541            let doc2 = tys !! 1
542            in custom ("Type" <+> doc2 <+> "does not contain all literals below" <+> (doc1 <> "."))
543
544          PFLiteral ->
545            case ts of
546              ~[m,n,_r,_a] ->
547                 let frac = backticks (ppWithNamesPrec names 4 m <> "/" <>
548                                       ppWithNamesPrec names 4 n)
549                     ty   = tys !! 3
550                 in custom (frac <+> "is not a valid literal of type" <+> ty)
551
552          PValidFloat ->
553            case ts of
554              ~[e,p] ->
555                custom ("Unsupported floating point parameters:" $$
556                     nest 2 ("exponent =" <+> ppWithNames names e $$
557                             "precision =" <+> ppWithNames names p))
558
559
560          PAnd        -> useCtr
561          PTrue       -> useCtr
562
563      _ -> useCtr
564
565
566
567
568-- | This picks the names to use when showing errors and warnings.
569computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap
570computeFreeVarNames warns errs =
571  mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars
572
573  {- XXX: Currently we pick the names based on the unique of the variable:
574     smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`)
575     This may still lead to changes in the names if the uniques got reordered
576     for some reason.  A more stable approach might be to order the variables
577     on their location in the error/warning, but that's quite a bit more code
578     so for now we just go with the simple approximation. -}
579
580  where
581  mkName x v = (tvUnique x, v)
582  mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots))
583
584  (numVaras,otherVars) = partition ((== KNum) . kindOf)
585                       $ Set.toList
586                       $ Set.filter isFreeTV
587                       $ fvs (map snd warns, map snd errs)
588
589  otherRoots = [ "a", "b", "c", "d" ]
590  numRoots   = [ "m", "n", "u", "v" ]
591
592  useUnicode = True
593
594  suff n
595    | n < 10 && useUnicode = [toEnum (0x2080 + n)]
596    | otherwise = show n
597
598  variant n x = if n == 0 then x else x ++ suff n
599
600  variants roots = [ variant n r | n <- [ 0 .. ], r <- roots ]
601