1-- | 2-- Module : Cryptol.TypeCheck.Monad 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8{-# LANGUAGE Safe #-} 9{-# LANGUAGE BangPatterns #-} 10{-# LANGUAGE DeriveAnyClass #-} 11{-# LANGUAGE DeriveGeneric #-} 12{-# LANGUAGE RecordWildCards #-} 13{-# LANGUAGE RecursiveDo #-} 14{-# LANGUAGE PatternGuards #-} 15{-# LANGUAGE OverloadedStrings #-} 16module Cryptol.TypeCheck.Monad 17 ( module Cryptol.TypeCheck.Monad 18 , module Cryptol.TypeCheck.InferTypes 19 ) where 20 21import Cryptol.ModuleSystem.Name 22 (FreshM(..),Supply,mkParameter 23 , nameInfo, NameInfo(..),NameSource(..)) 24import Cryptol.Parser.Position 25import qualified Cryptol.Parser.AST as P 26import Cryptol.TypeCheck.AST 27import Cryptol.TypeCheck.Subst 28import Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..)) 29import Cryptol.TypeCheck.InferTypes 30import Cryptol.TypeCheck.Error( Warning(..),Error(..) 31 , cleanupErrors, computeFreeVarNames 32 ) 33import qualified Cryptol.TypeCheck.SimpleSolver as Simple 34import qualified Cryptol.TypeCheck.Solver.SMT as SMT 35import Cryptol.TypeCheck.PP(NameMap) 36import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets) 37import Cryptol.Utils.Ident(Ident) 38import Cryptol.Utils.Panic(panic) 39 40import qualified Control.Applicative as A 41import qualified Control.Monad.Fail as Fail 42import Control.Monad.Fix(MonadFix(..)) 43import qualified Data.Map as Map 44import qualified Data.Set as Set 45import Data.Map (Map) 46import Data.Set (Set) 47import Data.List(find, foldl') 48import Data.Maybe(mapMaybe,fromMaybe) 49import MonadLib hiding (mapM) 50 51import Data.IORef 52 53 54import GHC.Generics (Generic) 55import Control.DeepSeq 56 57-- | Information needed for type inference. 58data InferInput = InferInput 59 { inpRange :: Range -- ^ Location of program source 60 , inpVars :: Map Name Schema -- ^ Variables that are in scope 61 , inpTSyns :: Map Name TySyn -- ^ Type synonyms that are in scope 62 , inpNewtypes :: Map Name Newtype -- ^ Newtypes in scope 63 , inpAbstractTypes :: Map Name AbstractType -- ^ Abstract types in scope 64 65 -- When typechecking a module these start off empty. 66 -- We need them when type-checking an expression at the command 67 -- line, for example. 68 , inpParamTypes :: !(Map Name ModTParam) -- ^ Type parameters 69 , inpParamConstraints :: !([Located Prop]) -- ^ Constraints on parameters 70 , inpParamFuns :: !(Map Name ModVParam) -- ^ Value parameters 71 72 73 , inpNameSeeds :: NameSeeds -- ^ Private state of type-checker 74 , inpMonoBinds :: Bool -- ^ Should local bindings without 75 -- signatures be monomorphized? 76 77 , inpCallStacks :: Bool -- ^ Are we tracking call stacks? 78 79 , inpSolverConfig :: SolverConfig -- ^ Options for the constraint solver 80 , inpSearchPath :: [FilePath] 81 -- ^ Where to look for Cryptol theory file. 82 83 , inpPrimNames :: !PrimMap 84 -- ^ This is used when the type-checker needs to refer to a predefined 85 -- identifier (e.g., @number@). 86 87 , inpSupply :: !Supply -- ^ The supply for fresh name generation 88 89 , inpSolver :: SMT.Solver -- ^ Solver connection for typechecking 90 } 91 92-- | This is used for generating various names. 93data NameSeeds = NameSeeds 94 { seedTVar :: !Int 95 , seedGoal :: !Int 96 } deriving (Show, Generic, NFData) 97 98-- | The initial seeds, used when checking a fresh program. 99-- XXX: why does this start at 10? 100nameSeeds :: NameSeeds 101nameSeeds = NameSeeds { seedTVar = 10, seedGoal = 0 } 102 103 104-- | The results of type inference. 105data InferOutput a 106 = InferFailed NameMap [(Range,Warning)] [(Range,Error)] 107 -- ^ We found some errors 108 109 | InferOK NameMap [(Range,Warning)] NameSeeds Supply a 110 -- ^ Type inference was successful. 111 112 113 deriving Show 114 115bumpCounter :: InferM () 116bumpCounter = do RO { .. } <- IM ask 117 io $ modifyIORef' iSolveCounter (+1) 118 119runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) 120runInferM info (IM m) = 121 do counter <- newIORef 0 122 rec ro <- return RO { iRange = inpRange info 123 , iVars = Map.map ExtVar (inpVars info) 124 , iTVars = [] 125 , iTSyns = fmap mkExternal (inpTSyns info) 126 , iNewtypes = fmap mkExternal (inpNewtypes info) 127 , iAbstractTypes = mkExternal <$> inpAbstractTypes info 128 , iParamTypes = inpParamTypes info 129 , iParamFuns = inpParamFuns info 130 , iParamConstraints = inpParamConstraints info 131 132 , iSolvedHasLazy = iSolvedHas finalRW -- RECURSION 133 , iMonoBinds = inpMonoBinds info 134 , iCallStacks = inpCallStacks info 135 , iSolver = inpSolver info 136 , iPrimNames = inpPrimNames info 137 , iSolveCounter = counter 138 } 139 140 (result, finalRW) <- runStateT rw 141 $ runReaderT ro m -- RECURSION 142 143 let theSu = iSubst finalRW 144 defSu = defaultingSubst theSu 145 warns = fmap' (fmap' (apSubst theSu)) (iWarnings finalRW) 146 147 case iErrors finalRW of 148 [] -> 149 case (iCts finalRW, iHasCts finalRW) of 150 (cts,[]) 151 | nullGoals cts -> inferOk warns 152 (iNameSeeds finalRW) 153 (iSupply finalRW) 154 (apSubst defSu result) 155 (cts,has) -> 156 inferFailed warns 157 [ ( goalRange g 158 , UnsolvedGoals [apSubst theSu g] 159 ) | g <- fromGoals cts ++ map hasGoal has 160 ] 161 162 errs -> inferFailed warns [(r,apSubst theSu e) | (r,e) <- errs] 163 164 where 165 inferOk ws a b c = pure (InferOK (computeFreeVarNames ws []) ws a b c) 166 inferFailed ws es = 167 let es1 = cleanupErrors es 168 in pure (InferFailed (computeFreeVarNames ws es1) ws es1) 169 170 171 mkExternal x = (IsExternal, x) 172 rw = RW { iErrors = [] 173 , iWarnings = [] 174 , iSubst = emptySubst 175 , iExistTVars = [] 176 177 , iNameSeeds = inpNameSeeds info 178 179 , iCts = emptyGoals 180 , iHasCts = [] 181 , iSolvedHas = Map.empty 182 183 , iSupply = inpSupply info 184 } 185 186 187 188 189 190 191 192newtype InferM a = IM { unIM :: ReaderT RO (StateT RW IO) a } 193 194data DefLoc = IsLocal | IsExternal 195 196-- | Read-only component of the monad. 197data RO = RO 198 { iRange :: Range -- ^ Source code being analysed 199 , iVars :: Map Name VarType -- ^ Type of variable that are in scope 200 201 {- NOTE: We assume no shadowing between these two, so it does not matter 202 where we look first. Similarly, we assume no shadowing with 203 the existential type variable (in RW). See 'checkTShadowing'. -} 204 205 , iTVars :: [TParam] -- ^ Type variable that are in scope 206 , iTSyns :: Map Name (DefLoc, TySyn) -- ^ Type synonyms that are in scope 207 , iNewtypes :: Map Name (DefLoc, Newtype) 208 -- ^ Newtype declarations in scope 209 -- 210 -- NOTE: type synonyms take precedence over newtype. The reason is 211 -- that we can define local type synonyms, but not local newtypes. 212 -- So, either a type-synonym shadows a newtype, or it was declared 213 -- at the top-level, but then there can't be a newtype with the 214 -- same name (this should be caught by the renamer). 215 , iAbstractTypes :: Map Name (DefLoc, AbstractType) 216 217 , iParamTypes :: Map Name ModTParam 218 -- ^ Parameter types 219 220 , iParamConstraints :: [Located Prop] 221 -- ^ Constraints on the type parameters 222 223 , iParamFuns :: Map Name ModVParam 224 -- ^ Parameter functions 225 226 227 , iSolvedHasLazy :: Map Int HasGoalSln 228 -- ^ NOTE: This field is lazy in an important way! It is the 229 -- final version of 'iSolvedHas' in 'RW', and the two are tied 230 -- together through recursion. The field is here so that we can 231 -- look thing up before they are defined, which is OK because we 232 -- don't need to know the results until everything is done. 233 234 , iMonoBinds :: Bool 235 -- ^ When this flag is set to true, bindings that lack signatures 236 -- in where-blocks will never be generalized. Bindings with type 237 -- signatures, and all bindings at top level are unaffected. 238 239 , iCallStacks :: Bool 240 -- ^ When this flag is true, retain source location information 241 -- in typechecked terms 242 243 , iSolver :: SMT.Solver 244 245 , iPrimNames :: !PrimMap 246 247 , iSolveCounter :: !(IORef Int) 248 } 249 250-- | Read-write component of the monad. 251data RW = RW 252 { iErrors :: ![(Range,Error)] -- ^ Collected errors 253 , iWarnings :: ![(Range,Warning)] -- ^ Collected warnings 254 , iSubst :: !Subst -- ^ Accumulated substitution 255 256 , iExistTVars :: [Map Name Type] 257 -- ^ These keeps track of what existential type variables are available. 258 -- When we start checking a function, we push a new scope for 259 -- its arguments, and we pop it when we are done checking the function 260 -- body. The front element of the list is the current scope, which is 261 -- the only thing that will be modified, as follows. When we encounter 262 -- a existential type variable: 263 -- 1. we look in all scopes to see if it is already defined. 264 -- 2. if it was not defined, we create a fresh type variable, 265 -- and we add it to the current scope. 266 -- 3. it is an error if we encounter an existential variable but we 267 -- have no current scope. 268 269 , iSolvedHas :: Map Int HasGoalSln 270 -- ^ Selector constraints that have been solved (ref. iSolvedSelectorsLazy) 271 272 -- Generating names 273 , iNameSeeds :: !NameSeeds 274 275 -- Constraints that need solving 276 , iCts :: !Goals -- ^ Ordinary constraints 277 , iHasCts :: ![HasGoal] 278 {- ^ Tuple/record projection constraints. The 'Int' is the "name" 279 of the constraint, used so that we can name its solution properly. -} 280 281 , iSupply :: !Supply 282 } 283 284instance Functor InferM where 285 fmap f (IM m) = IM (fmap f m) 286 287instance A.Applicative InferM where 288 pure = return 289 (<*>) = ap 290 291instance Monad InferM where 292 return x = IM (return x) 293 IM m >>= f = IM (m >>= unIM . f) 294 295instance Fail.MonadFail InferM where 296 fail x = IM (fail x) 297 298instance MonadFix InferM where 299 mfix f = IM (mfix (unIM . f)) 300 301instance FreshM InferM where 302 liftSupply f = IM $ 303 do rw <- get 304 let (a,s') = f (iSupply rw) 305 set rw { iSupply = s' } 306 return a 307 308 309io :: IO a -> InferM a 310io m = IM $ inBase m 311 312-- | The monadic computation is about the given range of source code. 313-- This is useful for error reporting. 314inRange :: Range -> InferM a -> InferM a 315inRange r (IM m) = IM $ mapReader (\ro -> ro { iRange = r }) m 316 317inRangeMb :: Maybe Range -> InferM a -> InferM a 318inRangeMb Nothing m = m 319inRangeMb (Just r) m = inRange r m 320 321-- | This is the current range that we are working on. 322curRange :: InferM Range 323curRange = IM $ asks iRange 324 325-- | Report an error. 326recordError :: Error -> InferM () 327recordError e = 328 do r <- case e of 329 AmbiguousSize d _ -> return (tvarSource d) 330 _ -> curRange 331 IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s } 332 333recordWarning :: Warning -> InferM () 334recordWarning w = 335 unless ignore $ 336 do r <- case w of 337 DefaultingTo d _ -> return (tvarSource d) 338 _ -> curRange 339 IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s } 340 where 341 ignore 342 | DefaultingTo d _ <- w 343 , Just n <- tvSourceName (tvarDesc d) 344 , Declared _ SystemName <- nameInfo n 345 = True 346 | otherwise = False 347 348getSolver :: InferM SMT.Solver 349getSolver = 350 do RO { .. } <- IM ask 351 return iSolver 352 353-- | Retrieve the mapping between identifiers and declarations in the prelude. 354getPrimMap :: InferM PrimMap 355getPrimMap = 356 do RO { .. } <- IM ask 357 return iPrimNames 358 359 360-------------------------------------------------------------------------------- 361newGoal :: ConstraintSource -> Prop -> InferM Goal 362newGoal goalSource goal = 363 do goalRange <- curRange 364 return Goal { .. } 365 366-- | Record some constraints that need to be solved. 367-- The string explains where the constraints came from. 368newGoals :: ConstraintSource -> [Prop] -> InferM () 369newGoals src ps = addGoals =<< mapM (newGoal src) ps 370 371{- | The constraints are removed, and returned to the caller. 372The substitution IS applied to them. -} 373getGoals :: InferM [Goal] 374getGoals = 375 do goals <- applySubst =<< 376 IM (sets $ \s -> (iCts s, s { iCts = emptyGoals })) 377 return (fromGoals goals) 378 379-- | Add a bunch of goals that need solving. 380addGoals :: [Goal] -> InferM () 381addGoals gs0 = doAdd =<< simpGoals gs0 382 where 383 doAdd [] = return () 384 doAdd gs = IM $ sets_ $ \s -> s { iCts = foldl' (flip insertGoal) (iCts s) gs } 385 386 387-- | Collect the goals emitted by the given sub-computation. 388-- Does not emit any new goals. 389collectGoals :: InferM a -> InferM (a, [Goal]) 390collectGoals m = 391 do origGs <- applySubst =<< getGoals' 392 a <- m 393 newGs <- getGoals 394 setGoals' origGs 395 return (a, newGs) 396 397 where 398 399 -- retrieve the type map only 400 getGoals' = IM $ sets $ \ RW { .. } -> (iCts, RW { iCts = emptyGoals, .. }) 401 402 -- set the type map directly 403 setGoals' gs = IM $ sets $ \ RW { .. } -> ((), RW { iCts = gs, .. }) 404 405simpGoal :: Goal -> InferM [Goal] 406simpGoal g = 407 case Simple.simplify mempty (goal g) of 408 p | Just t <- tIsError p -> 409 do recordError $ UnsolvableGoals [g { goal = t }] 410 return [] 411 | ps <- pSplitAnd p -> return [ g { goal = pr } | pr <- ps ] 412 413simpGoals :: [Goal] -> InferM [Goal] 414simpGoals gs = concat <$> mapM simpGoal gs 415 416 417 418{- | Record a constraint that when we select from the first type, 419we should get a value of the second type. 420The returned function should be used to wrap the expression from 421which we are selecting (i.e., the record or tuple). Plese note 422that the resulting expression should not be forced before the 423constraint is solved. 424-} 425newHasGoal :: P.Selector -> Type -> Type -> InferM HasGoalSln 426newHasGoal l ty f = 427 do goalName <- newGoalName 428 g <- newGoal CtSelector (pHas l ty f) 429 IM $ sets_ $ \s -> s { iHasCts = HasGoal goalName g : iHasCts s } 430 solns <- IM $ fmap iSolvedHasLazy ask 431 return $ case Map.lookup goalName solns of 432 Just e1 -> e1 433 Nothing -> panic "newHasGoal" ["Unsolved has goal in result"] 434 435 436-- | Add a previously generate has constrained 437addHasGoal :: HasGoal -> InferM () 438addHasGoal g = IM $ sets_ $ \s -> s { iHasCts = g : iHasCts s } 439 440-- | Get the @Has@ constraints. Each of this should either be solved, 441-- or added back using 'addHasGoal'. 442getHasGoals :: InferM [HasGoal] 443getHasGoals = do gs <- IM $ sets $ \s -> (iHasCts s, s { iHasCts = [] }) 444 applySubst gs 445 446-- | Specify the solution (@Expr -> Expr@) for the given constraint ('Int'). 447solveHasGoal :: Int -> HasGoalSln -> InferM () 448solveHasGoal n e = 449 IM $ sets_ $ \s -> s { iSolvedHas = Map.insert n e (iSolvedHas s) } 450 451 452-------------------------------------------------------------------------------- 453 454-- | Generate a fresh variable name to be used in a local binding. 455newParamName :: Ident -> InferM Name 456newParamName x = 457 do r <- curRange 458 liftSupply (mkParameter x r) 459 460newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a 461newName upd = IM $ sets $ \s -> let (x,seeds) = upd (iNameSeeds s) 462 in (x, s { iNameSeeds = seeds }) 463 464 465-- | Generate a new name for a goal. 466newGoalName :: InferM Int 467newGoalName = newName $ \s -> let x = seedGoal s 468 in (x, s { seedGoal = x + 1}) 469 470-- | Generate a new free type variable. 471newTVar :: TypeSource -> Kind -> InferM TVar 472newTVar src k = newTVar' src Set.empty k 473 474-- | Generate a new free type variable that depends on these additional 475-- type parameters. 476newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar 477newTVar' src extraBound k = 478 do r <- curRange 479 bound <- getBoundInScope 480 let vs = Set.union extraBound bound 481 msg = TVarInfo { tvarDesc = src, tvarSource = r } 482 newName $ \s -> let x = seedTVar s 483 in (TVFree x k vs msg, s { seedTVar = x + 1 }) 484 485 486-- | Check that the given "flavor" of parameter is allowed to 487-- have the given type, and raise an error if not 488checkParamKind :: TParam -> TPFlavor -> Kind -> InferM () 489 490checkParamKind tp flav k = 491 case flav of 492 TPModParam _ -> return () -- All kinds allowed as module parameters 493 TPPropSynParam _ -> starOrHashOrProp 494 TPTySynParam _ -> starOrHash 495 TPSchemaParam _ -> starOrHash 496 TPNewtypeParam _ -> starOrHash 497 TPPrimParam _ -> starOrHash 498 TPUnifyVar -> starOrHash 499 500 where 501 starOrHashOrProp = 502 case k of 503 KNum -> return () 504 KType -> return () 505 KProp -> return () 506 _ -> recordError (BadParameterKind tp k) 507 508 starOrHash = 509 case k of 510 KNum -> return () 511 KType -> return () 512 _ -> recordError (BadParameterKind tp k) 513 514 515-- | Generate a new free type variable. 516newTParam :: P.TParam Name -> TPFlavor -> Kind -> InferM TParam 517newTParam nm flav k = 518 do let desc = TVarInfo { tvarDesc = TVFromSignature (P.tpName nm) 519 , tvarSource = fromMaybe emptyRange (P.tpRange nm) 520 } 521 tp <- newName $ \s -> 522 let x = seedTVar s 523 in (TParam { tpUnique = x 524 , tpKind = k 525 , tpFlav = flav 526 , tpInfo = desc 527 } 528 , s { seedTVar = x + 1 }) 529 530 checkParamKind tp flav k 531 return tp 532 533 534-- | Generate an unknown type. The doc is a note about what is this type about. 535newType :: TypeSource -> Kind -> InferM Type 536newType src k = TVar `fmap` newTVar src k 537 538 539 540-------------------------------------------------------------------------------- 541 542 543-- | Record that the two types should be syntactically equal. 544unify :: TypeWithSource -> Type -> InferM [Prop] 545unify (WithSource t1 src) t2 = 546 do t1' <- applySubst t1 547 t2' <- applySubst t2 548 let ((su1, ps), errs) = runResult (mgu t1' t2') 549 extendSubst su1 550 let toError :: UnificationError -> Error 551 toError err = 552 case err of 553 UniTypeLenMismatch _ _ -> TypeMismatch src t1' t2' 554 UniTypeMismatch s1 s2 -> TypeMismatch src s1 s2 555 UniKindMismatch k1 k2 -> KindMismatch (Just src) k1 k2 556 UniRecursive x t -> RecursiveType src (TVar x) t 557 UniNonPolyDepends x vs -> TypeVariableEscaped src (TVar x) vs 558 UniNonPoly x t -> NotForAll src x t 559 case errs of 560 [] -> return ps 561 _ -> do mapM_ (recordError . toError) errs 562 return [] 563 564-- | Apply the accumulated substitution to something with free type variables. 565applySubst :: TVars t => t -> InferM t 566applySubst t = 567 do su <- getSubst 568 return (apSubst su t) 569 570applySubstPreds :: [Prop] -> InferM [Prop] 571applySubstPreds ps = 572 do ps1 <- applySubst ps 573 return (concatMap pSplitAnd ps1) 574 575 576applySubstGoals :: [Goal] -> InferM [Goal] 577applySubstGoals gs = 578 do gs1 <- applySubst gs 579 return [ g { goal = p } | g <- gs1, p <- pSplitAnd (goal g) ] 580 581-- | Get the substitution that we have accumulated so far. 582getSubst :: InferM Subst 583getSubst = IM $ fmap iSubst get 584 585-- | Add to the accumulated substitution, checking that the datatype 586-- invariant for 'Subst' is maintained. 587extendSubst :: Subst -> InferM () 588extendSubst su = 589 do mapM_ check (substToList su) 590 IM $ sets_ $ \s -> s { iSubst = su @@ iSubst s } 591 where 592 check :: (TVar, Type) -> InferM () 593 check (v, ty) = 594 case v of 595 TVBound _ -> 596 panic "Cryptol.TypeCheck.Monad.extendSubst" 597 [ "Substitution instantiates bound variable:" 598 , "Variable: " ++ show (pp v) 599 , "Type: " ++ show (pp ty) 600 ] 601 TVFree _ _ tvs _ -> 602 do let escaped = Set.difference (freeParams ty) tvs 603 if Set.null escaped then return () else 604 panic "Cryptol.TypeCheck.Monad.extendSubst" 605 [ "Escaped quantified variables:" 606 , "Substitution: " ++ show (pp v <+> text ":=" <+> pp ty) 607 , "Vars in scope: " ++ show (brackets (commaSep (map pp (Set.toList tvs)))) 608 , "Escaped: " ++ show (brackets (commaSep (map pp (Set.toList escaped)))) 609 ] 610 611 612-- | Variables that are either mentioned in the environment or in 613-- a selector constraint. 614varsWithAsmps :: InferM (Set TVar) 615varsWithAsmps = 616 do env <- IM $ fmap (Map.elems . iVars) ask 617 fromEnv <- forM env $ \v -> 618 case v of 619 ExtVar sch -> getVars sch 620 CurSCC _ t -> getVars t 621 sels <- IM $ fmap (map (goal . hasGoal) . iHasCts) get 622 fromSels <- mapM getVars sels 623 fromEx <- (getVars . concatMap Map.elems) =<< IM (fmap iExistTVars get) 624 return (Set.unions fromEnv `Set.union` Set.unions fromSels 625 `Set.union` fromEx) 626 where 627 getVars x = fvs `fmap` applySubst x 628 629-------------------------------------------------------------------------------- 630 631 632-- | Lookup the type of a variable. 633lookupVar :: Name -> InferM VarType 634lookupVar x = 635 do mb <- IM $ asks $ Map.lookup x . iVars 636 case mb of 637 Just t -> return t 638 Nothing -> 639 do mbNT <- lookupNewtype x 640 case mbNT of 641 Just nt -> return (ExtVar (newtypeConType nt)) 642 Nothing -> 643 do mbParamFun <- lookupParamFun x 644 case mbParamFun of 645 Just pf -> return (ExtVar (mvpType pf)) 646 Nothing -> panic "lookupVar" [ "Undefined type variable" 647 , show x] 648 649-- | Lookup a type variable. Return `Nothing` if there is no such variable 650-- in scope, in which case we must be dealing with a type constant. 651lookupTParam :: Name -> InferM (Maybe TParam) 652lookupTParam x = IM $ asks $ find this . iTVars 653 where this tp = tpName tp == Just x 654 655-- | Lookup the definition of a type synonym. 656lookupTSyn :: Name -> InferM (Maybe TySyn) 657lookupTSyn x = fmap (fmap snd . Map.lookup x) getTSyns 658 659-- | Lookup the definition of a newtype 660lookupNewtype :: Name -> InferM (Maybe Newtype) 661lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes 662 663lookupAbstractType :: Name -> InferM (Maybe AbstractType) 664lookupAbstractType x = fmap (fmap snd . Map.lookup x) getAbstractTypes 665 666-- | Lookup the kind of a parameter type 667lookupParamType :: Name -> InferM (Maybe ModTParam) 668lookupParamType x = Map.lookup x <$> getParamTypes 669 670-- | Lookup the schema for a parameter function. 671lookupParamFun :: Name -> InferM (Maybe ModVParam) 672lookupParamFun x = Map.lookup x <$> getParamFuns 673 674-- | Check if we already have a name for this existential type variable and, 675-- if so, return the definition. If not, try to create a new definition, 676-- if this is allowed. If not, returns nothing. 677 678existVar :: Name -> Kind -> InferM Type 679existVar x k = 680 do scopes <- iExistTVars <$> IM get 681 case msum (map (Map.lookup x) scopes) of 682 Just ty -> return ty 683 Nothing -> 684 case scopes of 685 [] -> 686 do recordError (UndefinedExistVar x) 687 newType TypeErrorPlaceHolder k 688 689 sc : more -> 690 do ty <- newType TypeErrorPlaceHolder k 691 IM $ sets_ $ \s -> s{ iExistTVars = Map.insert x ty sc : more } 692 return ty 693 694 695-- | Returns the type synonyms that are currently in scope. 696getTSyns :: InferM (Map Name (DefLoc,TySyn)) 697getTSyns = IM $ asks iTSyns 698 699-- | Returns the newtype declarations that are in scope. 700getNewtypes :: InferM (Map Name (DefLoc,Newtype)) 701getNewtypes = IM $ asks iNewtypes 702 703-- | Returns the abstract type declarations that are in scope. 704getAbstractTypes :: InferM (Map Name (DefLoc,AbstractType)) 705getAbstractTypes = IM $ asks iAbstractTypes 706 707-- | Returns the parameter functions declarations 708getParamFuns :: InferM (Map Name ModVParam) 709getParamFuns = IM $ asks iParamFuns 710 711-- | Returns the abstract function declarations 712getParamTypes :: InferM (Map Name ModTParam) 713getParamTypes = IM $ asks iParamTypes 714 715-- | Constraints on the module's parameters. 716getParamConstraints :: InferM [Located Prop] 717getParamConstraints = IM $ asks iParamConstraints 718 719-- | Get the set of bound type variables that are in scope. 720getTVars :: InferM (Set Name) 721getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars 722 723-- | Return the keys of the bound variables that are in scope. 724getBoundInScope :: InferM (Set TParam) 725getBoundInScope = 726 do ro <- IM ask 727 let params = Set.fromList (map mtpParam (Map.elems (iParamTypes ro))) 728 bound = Set.fromList (iTVars ro) 729 return $! Set.union params bound 730 731-- | Retrieve the value of the `mono-binds` option. 732getMonoBinds :: InferM Bool 733getMonoBinds = IM (asks iMonoBinds) 734 735getCallStacks :: InferM Bool 736getCallStacks = IM (asks iCallStacks) 737 738{- | We disallow shadowing between type synonyms and type variables 739because it is confusing. As a bonus, in the implementation we don't 740need to worry about where we lookup things (i.e., in the variable or 741type synonym environment. -} 742 743checkTShadowing :: String -> Name -> InferM () 744checkTShadowing this new = 745 do ro <- IM ask 746 rw <- IM get 747 let shadowed = 748 do _ <- Map.lookup new (iTSyns ro) 749 return "type synonym" 750 `mplus` 751 do guard (new `elem` mapMaybe tpName (iTVars ro)) 752 return "type variable" 753 `mplus` 754 do _ <- msum (map (Map.lookup new) (iExistTVars rw)) 755 return "type" 756 757 case shadowed of 758 Nothing -> return () 759 Just that -> 760 recordError (TypeShadowing this new that) 761 762 763 764-- | The sub-computation is performed with the given type parameter in scope. 765withTParam :: TParam -> InferM a -> InferM a 766withTParam p (IM m) = 767 do case tpName p of 768 Just x -> checkTShadowing "variable" x 769 Nothing -> return () 770 IM $ mapReader (\r -> r { iTVars = p : iTVars r }) m 771 772withTParams :: [TParam] -> InferM a -> InferM a 773withTParams ps m = foldr withTParam m ps 774 775-- | The sub-computation is performed with the given type-synonym in scope. 776withTySyn :: TySyn -> InferM a -> InferM a 777withTySyn t (IM m) = 778 do let x = tsName t 779 checkTShadowing "synonym" x 780 IM $ mapReader (\r -> r { iTSyns = Map.insert x (IsLocal,t) (iTSyns r) }) m 781 782withNewtype :: Newtype -> InferM a -> InferM a 783withNewtype t (IM m) = 784 IM $ mapReader 785 (\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t) 786 (iNewtypes r) }) m 787 788withPrimType :: AbstractType -> InferM a -> InferM a 789withPrimType t (IM m) = 790 IM $ mapReader 791 (\r -> r { iAbstractTypes = Map.insert (atName t) (IsLocal,t) 792 (iAbstractTypes r) }) m 793 794 795withParamType :: ModTParam -> InferM a -> InferM a 796withParamType a (IM m) = 797 IM $ mapReader 798 (\r -> r { iParamTypes = Map.insert (mtpName a) a (iParamTypes r) }) 799 m 800 801-- | The sub-computation is performed with the given variable in scope. 802withVarType :: Name -> VarType -> InferM a -> InferM a 803withVarType x s (IM m) = 804 IM $ mapReader (\r -> r { iVars = Map.insert x s (iVars r) }) m 805 806withVarTypes :: [(Name,VarType)] -> InferM a -> InferM a 807withVarTypes xs m = foldr (uncurry withVarType) m xs 808 809withVar :: Name -> Schema -> InferM a -> InferM a 810withVar x s = withVarType x (ExtVar s) 811 812-- | The sub-computation is performed with the given abstract function in scope. 813withParamFuns :: [ModVParam] -> InferM a -> InferM a 814withParamFuns xs (IM m) = 815 IM $ mapReader (\r -> r { iParamFuns = foldr add (iParamFuns r) xs }) m 816 where 817 add x = Map.insert (mvpName x) x 818 819-- | Add some assumptions for an entire module 820withParameterConstraints :: [Located Prop] -> InferM a -> InferM a 821withParameterConstraints ps (IM m) = 822 IM $ mapReader (\r -> r { iParamConstraints = ps ++ iParamConstraints r }) m 823 824 825-- | The sub-computation is performed with the given variables in scope. 826withMonoType :: (Name,Located Type) -> InferM a -> InferM a 827withMonoType (x,lt) = withVar x (Forall [] [] (thing lt)) 828 829-- | The sub-computation is performed with the given variables in scope. 830withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a 831withMonoTypes xs m = foldr withMonoType m (Map.toList xs) 832 833-- | The sub-computation is performed with the given type synonyms 834-- and variables in scope. 835withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a 836withDecls (ts,vs) m = foldr withTySyn (foldr add m (Map.toList vs)) ts 837 where 838 add (x,t) = withVar x t 839 840-- | Perform the given computation in a new scope (i.e., the subcomputation 841-- may use existential type variables). 842inNewScope :: InferM a -> InferM a 843inNewScope m = 844 do curScopes <- iExistTVars <$> IM get 845 IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes } 846 a <- m 847 IM $ sets_ $ \s -> s { iExistTVars = curScopes } 848 return a 849 850 851 852-------------------------------------------------------------------------------- 853-- Kind checking 854 855 856newtype KindM a = KM { unKM :: ReaderT KRO (StateT KRW InferM) a } 857 858data KRO = KRO { lazyTParams :: Map Name TParam -- ^ lazy map, with tparams. 859 , allowWild :: AllowWildCards -- ^ are type-wild cards allowed? 860 } 861 862-- | Do we allow wild cards in the given context. 863data AllowWildCards = AllowWildCards | NoWildCards 864 865data KRW = KRW { typeParams :: Map Name Kind -- ^ kinds of (known) vars. 866 , kCtrs :: [(ConstraintSource,[Prop])] 867 } 868 869instance Functor KindM where 870 fmap f (KM m) = KM (fmap f m) 871 872instance A.Applicative KindM where 873 pure = return 874 (<*>) = ap 875 876instance Monad KindM where 877 return x = KM (return x) 878 KM m >>= k = KM (m >>= unKM . k) 879 880instance Fail.MonadFail KindM where 881 fail x = KM (fail x) 882 883 884{- | The arguments to this function are as follows: 885 886(type param. name, kind signature (opt.), type parameter) 887 888The type parameter is just a thunk that we should not force. 889The reason is that the parameter depends on the kind that we are 890in the process of computing. 891 892As a result we return the value of the sub-computation and the computed 893kinds of the type parameters. -} 894runKindM :: AllowWildCards -- Are type-wild cards allowed? 895 -> [(Name, Maybe Kind, TParam)] -- ^ See comment 896 -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource,[Prop])]) 897runKindM wildOK vs (KM m) = 898 do (a,kw) <- runStateT krw (runReaderT kro m) 899 return (a, typeParams kw, kCtrs kw) 900 where 901 tps = Map.fromList [ (x,t) | (x,_,t) <- vs ] 902 kro = KRO { allowWild = wildOK, lazyTParams = tps } 903 krw = KRW { typeParams = Map.fromList [ (x,k) | (x,Just k,_) <- vs ] 904 , kCtrs = [] 905 } 906 907-- | This is what's returned when we lookup variables during kind checking. 908data LkpTyVar = TLocalVar TParam (Maybe Kind) -- ^ Locally bound variable. 909 | TOuterVar TParam -- ^ An outer binding. 910 911-- | Check if a name refers to a type variable. 912kLookupTyVar :: Name -> KindM (Maybe LkpTyVar) 913kLookupTyVar x = KM $ 914 do vs <- lazyTParams `fmap` ask 915 ss <- get 916 case Map.lookup x vs of 917 Just t -> return $ Just $ TLocalVar t $ Map.lookup x $ typeParams ss 918 Nothing -> lift $ lift $ do t <- lookupTParam x 919 return (fmap TOuterVar t) 920 921-- | Are type wild-cards OK in this context? 922kWildOK :: KindM AllowWildCards 923kWildOK = KM $ fmap allowWild ask 924 925-- | Reports an error. 926kRecordError :: Error -> KindM () 927kRecordError e = kInInferM $ recordError e 928 929kRecordWarning :: Warning -> KindM () 930kRecordWarning w = kInInferM $ recordWarning w 931 932kIO :: IO a -> KindM a 933kIO m = KM $ lift $ lift $ io m 934 935-- | Generate a fresh unification variable of the given kind. 936-- NOTE: We do not simplify these, because we end up with bottom. 937-- See `Kind.hs` 938-- XXX: Perhaps we can avoid the recursion? 939kNewType :: TypeSource -> Kind -> KindM Type 940kNewType src k = 941 do tps <- KM $ do vs <- asks lazyTParams 942 return $ Set.fromList (Map.elems vs) 943 kInInferM $ TVar `fmap` newTVar' src tps k 944 945-- | Lookup the definition of a type synonym. 946kLookupTSyn :: Name -> KindM (Maybe TySyn) 947kLookupTSyn x = kInInferM $ lookupTSyn x 948 949-- | Lookup the definition of a newtype. 950kLookupNewtype :: Name -> KindM (Maybe Newtype) 951kLookupNewtype x = kInInferM $ lookupNewtype x 952 953kLookupParamType :: Name -> KindM (Maybe ModTParam) 954kLookupParamType x = kInInferM (lookupParamType x) 955 956kLookupAbstractType :: Name -> KindM (Maybe AbstractType) 957kLookupAbstractType x = kInInferM $ lookupAbstractType x 958 959kExistTVar :: Name -> Kind -> KindM Type 960kExistTVar x k = kInInferM $ existVar x k 961 962-- | Replace the given bound variables with concrete types. 963kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type 964kInstantiateT t as = return (apSubst su t) 965 where su = listParamSubst as 966 967{- | Record the kind for a local type variable. 968This assumes that we already checked that there was no other valid 969kind for the variable (if there was one, it gets over-written). -} 970kSetKind :: Name -> Kind -> KindM () 971kSetKind v k = KM $ sets_ $ \s -> s{ typeParams = Map.insert v k (typeParams s)} 972 973-- | The sub-computation is about the given range of the source code. 974kInRange :: Range -> KindM a -> KindM a 975kInRange r (KM m) = KM $ 976 do e <- ask 977 s <- get 978 (a,s1) <- lift $ lift $ inRange r $ runStateT s $ runReaderT e m 979 set s1 980 return a 981 982kNewGoals :: ConstraintSource -> [Prop] -> KindM () 983kNewGoals _ [] = return () 984kNewGoals c ps = KM $ sets_ $ \s -> s { kCtrs = (c,ps) : kCtrs s } 985 986kInInferM :: InferM a -> KindM a 987kInInferM m = KM $ lift $ lift m 988