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