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