1-- | 2-- Module : Cryptol.TypeCheck.Kind 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE RecursiveDo #-} 10{-# LANGUAGE Safe #-} 11module Cryptol.TypeCheck.Kind 12 ( checkType 13 , checkSchema 14 , checkNewtype 15 , checkPrimType 16 , checkTySyn 17 , checkPropSyn 18 , checkParameterType 19 , checkParameterConstraints 20 ) where 21 22import qualified Cryptol.Parser.AST as P 23import Cryptol.Parser.Position 24import Cryptol.TypeCheck.AST 25import Cryptol.TypeCheck.Error 26import Cryptol.TypeCheck.Monad hiding (withTParams) 27import Cryptol.TypeCheck.SimpType(tRebuild) 28import Cryptol.TypeCheck.SimpleSolver(simplify) 29import Cryptol.TypeCheck.Solve (simplifyAllConstraints) 30import Cryptol.TypeCheck.Subst(listSubst,apSubst) 31import Cryptol.Utils.Panic (panic) 32import Cryptol.Utils.RecordMap 33 34import qualified Data.Map as Map 35import Data.List(sortBy,groupBy) 36import Data.Maybe(fromMaybe) 37import Data.Function(on) 38import Data.Text (Text) 39import Control.Monad(unless,when) 40 41 42 43-- | Check a type signature. Returns validated schema, and any implicit 44-- constraints that we inferred. 45checkSchema :: AllowWildCards -> P.Schema Name -> InferM (Schema, [Goal]) 46checkSchema withWild (P.Forall xs ps t mb) = 47 do ((xs1,(ps1,t1)), gs) <- 48 collectGoals $ 49 rng $ withTParams withWild schemaParam xs $ 50 do ps1 <- mapM checkProp ps 51 t1 <- doCheckType t (Just KType) 52 return (ps1,t1) 53 -- XXX: We probably shouldn't do this, as we are changing what the 54 -- user is doing. We do it so that things are in a propal normal form, 55 -- but we should probably figure out another time to do this. 56 let newPs = concatMap pSplitAnd $ map (simplify mempty) 57 $ map tRebuild ps1 58 return ( Forall xs1 newPs (tRebuild t1) 59 , [ g { goal = tRebuild (goal g) } | g <- gs ] 60 ) 61 62 where 63 rng = case mb of 64 Nothing -> id 65 Just r -> inRange r 66 67-- | Check a module parameter declarations. Nothing much to check, 68-- we just translate from one syntax to another. 69checkParameterType :: P.ParameterType Name -> Maybe Text -> InferM ModTParam 70checkParameterType a mbDoc = 71 do let k = cvtK (P.ptKind a) 72 n = thing (P.ptName a) 73 return ModTParam { mtpKind = k, mtpName = n, mtpDoc = mbDoc 74 , mtpNumber = P.ptNumber a } 75 76 77-- | Check a type-synonym declaration. 78checkTySyn :: P.TySyn Name -> Maybe Text -> InferM TySyn 79checkTySyn (P.TySyn x _ as t) mbD = 80 do ((as1,t1),gs) <- collectGoals 81 $ inRange (srcRange x) 82 $ do r <- withTParams NoWildCards tySynParam as 83 (doCheckType t Nothing) 84 simplifyAllConstraints 85 return r 86 return TySyn { tsName = thing x 87 , tsParams = as1 88 , tsConstraints = map (tRebuild . goal) gs 89 , tsDef = tRebuild t1 90 , tsDoc = mbD 91 } 92 93-- | Check a constraint-synonym declaration. 94checkPropSyn :: P.PropSyn Name -> Maybe Text -> InferM TySyn 95checkPropSyn (P.PropSyn x _ as ps) mbD = 96 do ((as1,t1),gs) <- collectGoals 97 $ inRange (srcRange x) 98 $ do r <- withTParams NoWildCards propSynParam as 99 (traverse checkProp ps) 100 simplifyAllConstraints 101 return r 102 return TySyn { tsName = thing x 103 , tsParams = as1 104 , tsConstraints = map (tRebuild . goal) gs 105 , tsDef = tRebuild (pAnd t1) 106 , tsDoc = mbD 107 } 108 109-- | Check a newtype declaration. 110-- XXX: Do something with constraints. 111checkNewtype :: P.Newtype Name -> Maybe Text -> InferM Newtype 112checkNewtype (P.Newtype x as fs) mbD = 113 do ((as1,fs1),gs) <- collectGoals $ 114 inRange (srcRange x) $ 115 do r <- withTParams NoWildCards newtypeParam as $ 116 flip traverseRecordMap fs $ \_n (rng,f) -> 117 kInRange rng $ doCheckType f (Just KType) 118 simplifyAllConstraints 119 return r 120 121 return Newtype { ntName = thing x 122 , ntParams = as1 123 , ntConstraints = map goal gs 124 , ntFields = fs1 125 , ntDoc = mbD 126 } 127 128checkPrimType :: P.PrimType Name -> Maybe Text -> InferM AbstractType 129checkPrimType p mbD = 130 do let (as,cs) = P.primTCts p 131 (as',cs') <- withTParams NoWildCards TPPrimParam as $ 132 mapM checkProp cs 133 pure AbstractType { atName = thing (P.primTName p) 134 , atKind = cvtK (thing (P.primTKind p)) 135 , atFixitiy = P.primTFixity p 136 , atCtrs = (as',cs') 137 , atDoc = mbD 138 } 139 140checkType :: P.Type Name -> Maybe Kind -> InferM Type 141checkType t k = 142 do (_, t1) <- withTParams AllowWildCards schemaParam [] $ doCheckType t k 143 return (tRebuild t1) 144 145checkParameterConstraints :: [Located (P.Prop Name)] -> InferM [Located Prop] 146checkParameterConstraints ps = 147 do (_, cs) <- withTParams NoWildCards schemaParam [] (mapM checkL ps) 148 return cs 149 where 150 checkL x = do p <- checkProp (thing x) 151 return x { thing = tRebuild p } 152 153 154{- | Check something with type parameters. 155 156When we check things with type parameters (i.e., type schemas, and type 157synonym declarations) we do kind inference based only on the immediately 158visible body. Type parameters that are not mentioned in the body are 159defaulted to kind 'KNum'. If this is not the desired behavior, programmers 160may add explicit kind annotations on the type parameters. 161 162Here is an example of how this may show up: 163 164> f : {n}. [8] -> [8] 165> f x = x + `n 166 167Note that @n@ does not appear in the body of the schema, so we will 168default it to 'KNum', which is the correct thing in this case. 169To use such a function, we'd have to provide an explicit type application: 170 171> f `{n = 3} 172 173There are two reasons for this choice: 174 175 1. It makes it possible to figure if something is correct without 176 having to look through arbitrary amounts of code. 177 178 2. It is a bit easier to implement, and it covers the large majority 179 of use cases, with a very small inconvenience (an explicit kind 180 annotation) in the rest. 181-} 182 183withTParams :: AllowWildCards {- ^ Do we allow wild cards -} -> 184 (Name -> TPFlavor) {- ^ What sort of params are these? -} -> 185 [P.TParam Name] {- ^ The params -} -> 186 KindM a {- ^ do this using the params -} -> 187 InferM ([TParam], a) 188withTParams allowWildCards flav xs m 189 | not (null duplicates) = panic "withTParams" $ "Repeated parameters" 190 : map show duplicates 191 | otherwise = 192 do (as,a,ctrs) <- 193 mdo (a, vars,ctrs) <- runKindM allowWildCards (zip' xs as) m 194 as <- mapM (newTP vars) xs 195 return (as,a,ctrs) 196 mapM_ (uncurry newGoals) ctrs 197 return (as,a) 198 199 where 200 getKind vs tp = 201 case Map.lookup (P.tpName tp) vs of 202 Just k -> return k 203 Nothing -> do recordWarning (DefaultingKind tp P.KNum) 204 return KNum 205 206 newTP vs tp = do k <- getKind vs tp 207 let nm = P.tpName tp 208 newTParam tp (flav nm) k 209 210 211 {- Note that we only zip based on the first argument. 212 This is needed to make the monadic recursion work correctly, 213 because the data dependency is only on the part that is known. -} 214 zip' [] _ = [] 215 zip' (a:as) ~(t:ts) = (P.tpName a, fmap cvtK (P.tpKind a), t) : zip' as ts 216 217 duplicates = [ ds | ds@(_ : _ : _) <- groupBy ((==) `on` P.tpName) 218 $ sortBy (compare `on` P.tpName) xs ] 219 220cvtK :: P.Kind -> Kind 221cvtK P.KNum = KNum 222cvtK P.KType = KType 223cvtK P.KProp = KProp 224cvtK (P.KFun k1 k2) = cvtK k1 :-> cvtK k2 225 226 227 228-- | Check an application of a type constant. 229tcon :: TCon -- ^ Type constant being applied 230 -> [P.Type Name] -- ^ Type parameters 231 -> Maybe Kind -- ^ Expected kind 232 -> KindM Type -- ^ Resulting type 233tcon tc ts0 k = 234 do (ts1,k1) <- appTy ts0 (kindOf tc) 235 checkKind (TCon tc ts1) k k1 236 237 238-- | Check a type application of a non built-in type or type variable. 239checkTUser :: 240 Name {- ^ The name that is being applied to some arguments. -} -> 241 [P.Type Name] {- ^ Parameters to the type -} -> 242 Maybe Kind {- ^ Expected kind -} -> 243 KindM Type {- ^ Resulting type -} 244checkTUser x ts k = 245 mcase kLookupTyVar checkBoundVarUse $ 246 mcase kLookupTSyn checkTySynUse $ 247 mcase kLookupNewtype checkNewTypeUse $ 248 mcase kLookupParamType checkModuleParamUse $ 249 mcase kLookupAbstractType checkAbstractTypeUse $ 250 checkScopedVarUse -- none of the above, must be a scoped type variable, 251 -- if the renamer did its job correctly. 252 where 253 checkTySynUse tysyn = 254 do (ts1,k1) <- appTy ts (kindOf tysyn) 255 let as = tsParams tysyn 256 ts2 <- checkParams as ts1 257 let su = zip as ts2 258 ps1 <- mapM (`kInstantiateT` su) (tsConstraints tysyn) 259 kNewGoals (CtPartialTypeFun (tsName tysyn)) ps1 260 t1 <- kInstantiateT (tsDef tysyn) su 261 checkKind (TUser x ts1 t1) k k1 262 263 checkNewTypeUse nt = 264 do (ts1,k1) <- appTy ts (kindOf nt) 265 let as = ntParams nt 266 ts2 <- checkParams as ts1 267 let su = zip as ts2 268 ps1 <- mapM (`kInstantiateT` su) (ntConstraints nt) 269 kNewGoals (CtPartialTypeFun (ntName nt)) ps1 270 checkKind (TNewtype nt ts2) k k1 271 272 checkAbstractTypeUse absT = 273 do let tc = abstractTypeTC absT 274 (ts1,k1) <- appTy ts (kindOf tc) 275 let (as,ps) = atCtrs absT 276 case ps of 277 [] -> pure () -- common case 278 _ -> do let need = length as 279 have = length ts1 280 when (need > have) $ 281 kRecordError (TooFewTyParams (atName absT) (need - have)) 282 let su = listSubst (map tpVar as `zip` ts1) 283 kNewGoals (CtPartialTypeFun (atName absT)) (apSubst su <$> ps) 284 checkKind (TCon tc ts1) k k1 285 286 checkParams as ts1 287 | paramHave == paramNeed = return ts1 288 | paramHave < paramNeed = 289 do kRecordError (TooFewTyParams x (paramNeed-paramHave)) 290 let src = TypeErrorPlaceHolder 291 fake <- mapM (kNewType src . kindOf . tpVar) 292 (drop paramHave as) 293 return (ts1 ++ fake) 294 | otherwise = do kRecordError (TooManyTySynParams x (paramHave-paramNeed)) 295 return (take paramNeed ts1) 296 where paramHave = length ts1 297 paramNeed = length as 298 299 300 301 checkModuleParamUse a = 302 do let ty = tpVar (mtpParam a) 303 (ts1,k1) <- appTy ts (kindOf ty) 304 case k of 305 Just ks | ks /= k1 -> kRecordError $ KindMismatch Nothing ks k1 306 _ -> return () 307 308 unless (null ts1) $ 309 panic "Kind.checkTUser.checkModuleParam" [ "Unexpected parameters" ] 310 311 return (TVar ty) 312 313 checkBoundVarUse v = 314 do unless (null ts) $ kRecordError TyVarWithParams 315 case v of 316 TLocalVar t mbk -> 317 case k of 318 Nothing -> return (TVar (tpVar t)) 319 Just k1 -> 320 case mbk of 321 Nothing -> kSetKind x k1 >> return (TVar (tpVar t)) 322 Just k2 -> checkKind (TVar (tpVar t)) k k2 323 TOuterVar t -> checkKind (TVar (tpVar t)) k (kindOf t) 324 325 checkScopedVarUse = 326 do unless (null ts) (kRecordError TyVarWithParams) 327 kExistTVar x $ fromMaybe KNum k 328 329 mcase :: (Name -> KindM (Maybe a)) -> 330 (a -> KindM Type) -> 331 KindM Type -> 332 KindM Type 333 mcase m f rest = 334 do mb <- m x 335 case mb of 336 Nothing -> rest 337 Just a -> f a 338 339-- | Check a type-application. 340appTy :: [P.Type Name] -- ^ Parameters to type function 341 -> Kind -- ^ Kind of type function 342 -> KindM ([Type], Kind) -- ^ Validated parameters, resulting kind 343appTy [] k1 = return ([],k1) 344 345appTy (t : ts) (k1 :-> k2) = 346 do t1 <- doCheckType t (Just k1) 347 (ts1,k) <- appTy ts k2 348 return (t1 : ts1, k) 349 350appTy ts k1 = 351 do kRecordError (TooManyTypeParams (length ts) k1) 352 return ([], k1) 353 354 355-- | Validate a parsed type. 356doCheckType :: P.Type Name -- ^ Type that needs to be checked 357 -> Maybe Kind -- ^ Expected kind (if any) 358 -> KindM Type -- ^ Checked type 359doCheckType ty k = 360 case ty of 361 P.TWild -> 362 do wildOk <- kWildOK 363 case wildOk of 364 AllowWildCards -> return () 365 NoWildCards -> kRecordError UnexpectedTypeWildCard 366 theKind <- case k of 367 Just k1 -> return k1 368 Nothing -> do kRecordWarning (DefaultingWildType P.KNum) 369 return KNum 370 kNewType TypeWildCard theKind 371 372 P.TFun t1 t2 -> tcon (TC TCFun) [t1,t2] k 373 P.TSeq t1 t2 -> tcon (TC TCSeq) [t1,t2] k 374 P.TBit -> tcon (TC TCBit) [] k 375 P.TNum n -> tcon (TC (TCNum n)) [] k 376 P.TChar n -> tcon (TC (TCNum $ toInteger $ fromEnum n)) [] k 377 378 P.TTuple ts -> tcon (TC (TCTuple (length ts))) ts k 379 380 P.TRecord fs -> do t1 <- TRec <$> traverseRecordMap checkF fs 381 checkKind t1 k KType 382 P.TLocated t r1 -> kInRange r1 $ doCheckType t k 383 384 P.TUser x ts -> checkTUser x ts k 385 386 P.TParens t -> doCheckType t k 387 388 P.TInfix t x _ u-> doCheckType (P.TUser (thing x) [t, u]) k 389 390 P.TTyApp _fs -> do kRecordError BareTypeApp 391 kNewType TypeWildCard KNum 392 393 where 394 checkF _nm (rng,v) = kInRange rng $ doCheckType v (Just KType) 395 396-- | Validate a parsed proposition. 397checkProp :: P.Prop Name -- ^ Proposition that need to be checked 398 -> KindM Type -- ^ Checked representation 399checkProp (P.CType t) = doCheckType t (Just KProp) 400 401 402-- | Check that a type has the expected kind. 403checkKind :: Type -- ^ Kind-checked type 404 -> Maybe Kind -- ^ Expected kind (if any) 405 -> Kind -- ^ Inferred kind 406 -> KindM Type -- ^ A type consistent with expectations. 407checkKind _ (Just k1) k2 408 | k1 /= k2 = do kRecordError (KindMismatch Nothing k1 k2) 409 kNewType TypeErrorPlaceHolder k1 410checkKind t _ _ = return t 411 412 413