module ContextErrors ( handleContextReduction, handleWeakContext, handleAmbiguousContext, updateContexts ) where import Data.List import qualified Data.Set as S import Control.Monad(when) import Position import Error(internalError, EMsg, ErrMsg(..)) import PFPrint import Pred import Subst(Types(..)) import TIMonad import TCMisc import Unify import FStringCompat (mkFString) import Id(mkId) import PreIds import CSyntax import Util(separate, concatMapM, quote, headOrErr, toMaybe, boolCompress) import CType(typeclassId, isTNum, getTNum) --import Debug.Trace -- ======================================================================== -- Context Reduction -- -- -- Given a position where the context reduction failed and -- a list of the contexts which failed to reduce, this function -- returns the list of error messages which should be reported -- handleContextReduction :: Position -> [VPred] -> TI a handleContextReduction pos vps = do -- We used to remove duplicates: -- let vps' = nubVPred vps -- Now this is covered under the following filter, which removes -- predicates that are implied by predicates already in the list. -- That way, we only report the predicates which need to be resolved -- (the others would be satisfied given the reported predicates). vps_noimpl <- removeImpliedPreds [] [] vps -- For each proviso, figure out whether it can be reduced, just -- not all the way (the inability to reduce a required proviso is -- the real stumbling point) vps_noimpl_reduced <- findReducedPreds [] vps_noimpl -- It is now safe to rename type variables to use nicer names -- (a__, b__, c__, etc) -- It was not safe to do so before, because some might have been -- bound variables and thus were named in the TI monad state -- which "findReducedPreds" used to simplify the preds. let vps_reduced_nicenames = niceTypes vps_noimpl_reduced -- we use to do messing around with PrimSelectable because it could -- introduce messed-up literal, etc. contexts -- now that indexing is rationalized, we expect that all the -- non-implied predicates are legitimate problems -- e.g. x[c] where x is not selectable and c is a clock -- x is an issue because you can't select from it and c -- is an issue because it is not a valid index for selection -- But now we do the same "messing around" for IsModule: -- Filter the IsModule predicates on "<-" let is_mod_arrow_vps = filter (isIsModuleArrow . fst) vps_reduced_nicenames -- if there are any, report only them, else report all the preds let err_vps = if (null is_mod_arrow_vps) then vps_reduced_nicenames else is_mod_arrow_vps emsgs <- mapM (handleContextReduction' pos) err_vps errs "handleContextReduction" emsgs -- -------------------- -- This helper function takes one predicate at a time handleContextReduction' :: Position -> (VPred, [VPred]) -> TI EMsg handleContextReduction' pos p@((VPred vpi (PredWithPositions (IsIn c@(Class { name=(CTypeclass cid) }) ts) _)), _) | cid == idBitwise = case ts of [t] -> return $ handleCtxRedBitwise pos p t _ -> internalError("handleContextReduction': " ++ "Bitwise instance contains wrong number of types") | cid == idBitReduce = case ts of [vec, sz] -> return $ handleCtxRedBitReduce pos p vec sz _ -> internalError("handleContextReduction': " ++ "Bitwise instance contains wrong number of types") | cid == idBits = case ts of [t,szt] -> case szt of (TCon (TyNum sz _)) -> handleCtxRedWrongBitSize pos p c t sz _ -> return $ defaultContextReductionErr pos p _ -> internalError("handleContextReduction': " ++ "Bits instance contains wrong number of types") | cid == idBitExtend = case ts of [szt1, szt2, t3] -> handleCtxRedBitExtend pos p c szt1 szt2 t3 _ -> internalError("handleContextReduction': " ++ "BitExtend instance contains wrong number of types") | cid == idPrimSelectable = case ts of [arr, val] -> handleCtxRedPrimSelectable pos p c arr val _ -> internalError ("handleContextReduction': " ++ "PrimSelectable instance contains wrong number of types") | cid == idPrimUpdateable = case ts of [arr, val] -> handleCtxRedPrimUpdateable pos p c arr val _ -> internalError ("handleContextReduction': " ++ "PrimUpdateable instance contains wrong number of types") | cid == idPrimWriteable = case ts of [arr, val] -> handleCtxRedPrimWriteable pos p c arr val _ -> internalError ("handleContextReduction': " ++ "PrimWriteable instance contains wrong number of types") | cid == idPrimIndex = case ts of [ix, sz] -> handleCtxRedPrimIndex pos p c ix sz _ -> internalError("handleContextReduction': " ++ "PrimIndex instance contains wrong number of types") | cid == idIsModule = case ts of [mt, ct] -> return $ handleCtxRedIsModule pos p mt ct _ -> internalError ("handleContextReduction': " ++ "IsModule instance contains wrong number of types") | cid == idNumEq = case ts of [t1, t2] -> return $ handleNotNumEq pos (getVPredPositions (fst p)) t1 t2 _ -> internalError ("handleContextReduction': " ++ "NumEq instance contains wrong number of types") | cid == idPrimParam = case ts of [t, tsz] -> return $ handleCtxRedPrimParam pos p t _ -> internalError("handleContextReduction': " ++ "PrimParam instance contains wrong number of types") | cid == idPrimPort = case ts of [t, tsz] -> return $ handleCtxRedPrimPort pos p t _ -> internalError("handleContextReduction': " ++ "PrimPort instance contains wrong number of types") | cid == idSizedLiteral = case ts of [t, szt] -> case szt of (TCon (TyNum sz _)) -> handleCtxRedWrongBitSize pos p c t sz _ -> return $ defaultContextReductionErr pos p _ -> internalError("handleContextReduction': " ++ "SizedLiteral instance contains wrong number of types") -- | cid == idLiteral = -- | cid == idRealLiteral = -- | cid == idStringLiteral = handleContextReduction' pos p = return (defaultContextReductionErr pos p) -- -------------------- defaultContextReductionErr :: Position -> (VPred, [VPred]) -> EMsg defaultContextReductionErr pos (p, reduced_ps) = let mkVarPos v = (pfpString v, getPosition v) -- now that we fail fast, "pos" could be in "poss", remove it poss = filterPositions pos $ getVPredPositions p pred = toPred p varposs = map mkVarPos (tv pred) in if null reduced_ps then (pos, EContextReduction (pfpString pred) poss varposs) else (pos, EContextReductionReduces (pfpString pred) (map (predToDescr . toPred) reduced_ps) poss varposs) -- -------------------- -- If the unreduced context is Bits for a known size, try to satisfy -- the context with a fresh variable replaced for the known size. If -- the context reduces, and the variable is bound to a specific size, -- then report an error about the mismatched size. handleCtxRedWrongBitSize :: Position -> (VPred, [VPred]) -> Class -> Type -> Integer -> TI EMsg handleCtxRedWrongBitSize pos (vp@(VPred vpi _), reduced_ps) c t sz = do let default_err = defaultContextReductionErr pos (vp, reduced_ps) szv <- newTVar "handleCtxRedWrongBitSize" KNum vpi let p' = IsIn c [t,szv] vp' = VPred vpi (PredWithPositions p' []) -- Use "satisfy", instead of "reducePred", because the size might -- result from arithmetic on the sizes of subtypes, via new predicates -- (so we need to continue until all preds are satisfied) (rs,_) <- satisfy [] [vp'] s <- getSubst let szv' = apSub s szv return $ if (null rs) && (isTNum szv') then wrongBitSizeErr pos vp t (getTNum szv') sz else default_err wrongBitSizeErr :: Position -> VPred -> Type -> Integer -> Integer -> EMsg wrongBitSizeErr pos p t tsz sz2 = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedWrongBitSize (pfpString t) tsz sz2 poss) -- -------------------- -- If bitwise operations are used on a Bool value, give a special warning. -- If any other concrete type the subject of bitwise operators, but there -- is no instance for it, then report a special error. If the type is a -- variable (presumably an ambiguous variable), report the default error. handleCtxRedBitwise :: Position -> (VPred, [VPred]) -> Type -> EMsg handleCtxRedBitwise pos (vp, reduced_ps) t = let poss = filterPositions pos $ getVPredPositions vp bwbool_err = (pos, ECtxRedBitwiseBool poss) bw_err = (pos, ECtxRedBitwise (pfpString t) poss) default_err = defaultContextReductionErr pos (vp, reduced_ps) in case t of TCon (TyCon i _ _) | i == idBool -> bwbool_err _ -> case (tv t) of [] -> bw_err _ -> -- let's assume that a proviso would work here default_err -- -------------------- handleCtxRedBitReduce :: Position -> (VPred, [VPred]) -> Type -> Type -> EMsg handleCtxRedBitReduce pos (vp, reduced_ps) vec_type vec_size = let poss = filterPositions pos $ getVPredPositions vp br_err = (pos, ECtxRedBitReduce (pfpString vec_type) poss) default_err = defaultContextReductionErr pos (vp, reduced_ps) in case (tv vec_type) of [] -> br_err _ -> -- let's assume that a proviso would work here default_err -- -------------------- -- Check to see if replacing the size types with variables matches any -- instance. If not, then the value type does not have -- extend/truncate defined for it. (This is a rare case, but what -- the heck, let's check for it.) If this passes, then check to see -- if the two numeric sizes are known. If so, and if sz1 > sz2, then -- the problem is bad sizes. handleCtxRedBitExtend :: Position -> (VPred, [VPred]) -> Class -> Type -> Type -> Type -> TI EMsg handleCtxRedBitExtend pos (vp@(VPred vpi _), reduced_ps) c szt1 szt2 t3 = do let poss = filterPositions pos $ getVPredPositions vp badsize_err sz1 sz2 = (pos, ECtxRedBitExtendBadSizes sz1 sz2 poss) badtype_err = (pos, ECtxRedBitExtendBadType (pfpString t3) poss) default_err = defaultContextReductionErr pos (vp, reduced_ps) szt1' <- newTVar "handleCtxRedBitExtend1" KNum vpi szt2' <- newTVar "handleCtxRedBitExtend2" KNum vpi let p' = IsIn c [szt1',szt2',t3] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' case x of (Just ([vp2], b, us, _)) | (vpClassIs (CTypeclass idAdd) vp2) -> case (szt1, szt2) of (TCon (TyNum sz1 _), TCon (TyNum sz2 _)) -> return (badsize_err sz1 sz2) _ -> return default_err _ -> return badtype_err -- -------------------- type PredError = Position -> VPred -> Type -> EMsg type ElemError = Position -> VPred -> Type -> Type -> Type -> EMsg notSelectableErr :: PredError notSelectableErr pos p t = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedNotSelectable (pfpString t) poss) wrongSelectionResultErr :: ElemError wrongSelectionResultErr pos p arr expected_val found_val = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedWrongSelectionResult (pfpString arr) (pfpString expected_val) (pfpString found_val) poss) notUpdateableErr :: PredError notUpdateableErr pos p t = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedNotUpdateable (pfpString t) poss) wrongUpdateArgErr :: ElemError wrongUpdateArgErr pos p arr expected_val found_val = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedWrongUpdateArg (pfpString arr) (pfpString expected_val) (pfpString found_val) poss) notWriteableErr :: PredError notWriteableErr pos p t = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedNotWriteable (pfpString t) poss) wrongWriteArgErr :: ElemError wrongWriteArgErr pos p arr expected_val found_val = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedWrongWriteArg (pfpString arr) (pfpString expected_val) (pfpString found_val) poss) -- handle context reduction errors for the [] contexts -- PrimSelectable, PrimUpdateable, PrimWriteable handleBracketCtxRed :: PredError -> ElemError -> Position -> (VPred, [VPred]) -> Class -> Type -> Type -> TI (EMsg) handleBracketCtxRed pred_error elem_error pos (vp@(VPred vpi _), _) c arr val = do -- create new val variable val_var <- newTVar "handleBracketCtxRed" KStar vpi let p' = IsIn c [arr, val_var] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' case x of -- there is an instance of the bracket class for type "arr" Just (ps, _, us, _) -> do -- there may be context with informative fundeps, so propagate them _ <- propagateFunDeps ps s <- getSubst let real_val = apSub us (apSub s val_var) return (elem_error pos vp arr real_val val) -- there is no instance of the class for type "arr" x -> return (pred_error pos vp arr) handleCtxRedPrimSelectable :: Position -> (VPred, [VPred]) -> Class -> Type -> Type -> TI EMsg handleCtxRedPrimSelectable = handleBracketCtxRed notSelectableErr wrongSelectionResultErr handleCtxRedPrimUpdateable :: Position -> (VPred, [VPred]) -> Class -> Type -> Type -> TI EMsg handleCtxRedPrimUpdateable = handleBracketCtxRed notUpdateableErr wrongUpdateArgErr handleCtxRedPrimWriteable :: Position -> (VPred, [VPred]) -> Class -> Type -> Type -> TI EMsg handleCtxRedPrimWriteable = handleBracketCtxRed notWriteableErr wrongWriteArgErr handleCtxRedPrimIndex :: Position -> (VPred, [VPred]) -> Class -> Type -> Type -> TI (EMsg) handleCtxRedPrimIndex pos (vp@(VPred vpi _), reduced_ps) c ix sz = do -- create new size variable sz_var <- newTVar "handleCtxRedPrimIndex" KNum vpi let p' = IsIn c [ix, sz_var] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' case x of -- there is an instance of PrimIndex for type "i" Just (_, _, us, _) -> let real_sz = (apSub us sz_var) in return (wrongIndexSizeErr pos (vp, reduced_ps) ix real_sz sz ) x -> return (notIndexTypeErr pos vp ix) notIndexTypeErr :: Position -> VPred -> Type -> EMsg notIndexTypeErr pos p t = let poss = filterPositions pos $ getVPredPositions p in (pos, ECtxRedBadSelectionIndex (pfpString t) poss) -- currently just generates a standard context reduction error -- but this could be improved if the issue actually turns up in -- user code wrongIndexSizeErr :: Position -> (VPred, [VPred]) -> Type -> Type -> Type -> EMsg wrongIndexSizeErr pos p ix real_sz sz = defaultContextReductionErr pos p -- -------------------- isIsModuleArrow :: VPred -> Bool isIsModuleArrow (VPred vpi (PredWithPositions (IsIn (Class { name=(CTypeclass cid) }) [mt, ct]) _)) | (cid == idIsModule) && (isArrow mt) = True isIsModuleArrow _ = False isArrow :: Type -> Bool isArrow t = case (leftCon t) of Just i | (i == idArrow noPosition) -> True _ -> False isActionValue :: Type -> Bool isActionValue (TCon (TyCon i _ _)) | (i == idActionValue) = True isActionValue _ = False handleCtxRedIsModule :: Position -> (VPred, [VPred]) -> Type -> Type -> EMsg handleCtxRedIsModule pos (vp, _) mt ct = let poss = filterPositions pos $ getVPredPositions vp in if (isArrow mt) then (pos, EModInstWrongArgs poss) else if (isActionValue mt) then (pos, ECtxRedIsModuleActionValue poss) else (pos, ECtxRedIsModule (pfpString mt) poss) -- -------------------- handleNotNumEq :: Position -> [Position] -> Type -> Type -> EMsg handleNotNumEq pos poss t1 t2 = (pos, ENotNumEq t1_str t2_str poss') where poss' = filterPositions pos poss t1_str = pfpString t1 t2_str = pfpString t2 -- -------------------- handleCtxRedPrimParam :: Position -> (VPred, [VPred]) -> Type -> EMsg handleCtxRedPrimParam pos (vp, reduced_ps) userty = let poss = filterPositions pos $ getVPredPositions vp hasVar = toMaybe (not (null (tv userty))) (map (pfpString . toPred) reduced_ps) in (pos, ECtxErrPrimParam (pfpString userty) poss hasVar) handleCtxRedPrimPort :: Position -> (VPred, [VPred]) -> Type -> EMsg handleCtxRedPrimPort pos (vp, reduced_ps) userty = let poss = filterPositions pos $ getVPredPositions vp hasVar = toMaybe (not (null (tv userty))) (map (pfpString . toPred) reduced_ps) in (pos, ECtxErrPrimPort (pfpString userty) poss hasVar) -- ======================================================================== -- Weak Context -- -- When adding new errors, remember to use "niceTypes" to convert -- mangled type variable names into letters. handleWeakContext :: Position -> Type -> [PredWithPositions] -> [Pred] -> [PredWithPositions] -> TI a handleWeakContext pos t qs ds rs = do -- traceM ("handleWeakContext qs: " ++ ppReadable qs) -- traceM ("handleWeakContext ds: " ++ ppReadable ds) -- traceM ("handleWeakContext rs: " ++ ppReadable rs) -- Only report the predicates which are necessary, not those -- which could be left off because other predicates imply them. rs_noimpl <- removeImpliedPredWPs qs ds rs -- traceM("handleWeakContext rs_noimpl: " ++ ppReadable rs_noimpl) -- For each proviso, figure out whether it can be reduced, just -- not all the way (the inability to reduce a required proviso is -- the real stumbling point) rs_noimpl_reduced <- findReducedPredWPs ds rs_noimpl xs <- mapM (handleWeakContext' pos t qs) rs_noimpl_reduced -- separate out the handled from the non-handled let (ctx_errs, rs') = separate xs -- traceM("handleWeakContext rs': " ++ ppReadable rs') -- report the remaining errors in one emsg let def_errs = [defaultWeakContextErr pos t qs rs' | not (null rs')] -- report the specific errors first errs "handleWeakContext" (ctx_errs ++ def_errs) handleWeakContext' :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakContext' pos t qs pwp@((PredWithPositions (IsIn (Class {name=(CTypeclass cid)}) ts) _), _) | cid == idBitExtend = handleWeakCtxBitExtend pos t qs pwp | cid == idPrimSelectable = handleWeakCtxPrimSelectable pos t qs pwp | cid == idPrimUpdateable = handleWeakCtxPrimUpdateable pos t qs pwp | cid == idPrimWriteable = handleWeakCtxPrimWriteable pos t qs pwp | cid == idPrimParam = handleWeakCtxPrimParam pos t qs pwp | cid == idPrimPort = handleWeakCtxPrimPort pos t qs pwp | cid == idNumEq = case ts of [t1, t2] -> return $ Left (handleNotNumEq pos (getPredPositions (fst pwp)) t1 t2) _ -> internalError ("handleWeakContext' NumEq: " ++ ppReadable (t,qs,pwp)) -- | cid == idPrimIndex = handleWeakCtxPrimIndex pos t qs pwp -- | cid == ... handleWeakContext' pos _ _ p = return (Right p) defaultWeakContextErr :: Position -> Type -> [PredWithPositions] -> [(PredWithPositions, [Pred])] -> EMsg defaultWeakContextErr pos t qs rs = let -- rename generated typevars with "a__", "b__", etc -- (should only be new tvars in the required preds) -- but skip any that are already in the user-given type (rs', qs', t') = niceTypes (rs, qs, t) -- find the tvars so that we can report a position for any -- generated tvars tvars = nub $ sort $ concat [tv (removePredPositions pred) | (pred, _) <- rs'] -- only report the location of generated tvars -- (niceTypes preserves the "isNewTVar" property) gen_tvars = filter isNewTVar tvars -- pair the renamed gen_tvars with their positions -- (only those which have a position) gen_tvars_with_positions = [(ppString t, tpos) | t <- gen_tvars, let tpos = getPosition t, tpos /= noPosition ] -- format the predicates for the error message mkinfo (p, ps) = (pfpString (removePredPositions p), getPredPositions p, map predToDescr ps) rps = map mkinfo rs' in (pos, EWeakContext (pfpString t') (map pfpString qs') rps gen_tvars_with_positions) -- -------------------- -- A BitExtend context could fail to resolve because the Add superclass -- requirement might be failing. If this is the only reason, report the -- Add class instead. handleWeakCtxBitExtend :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxBitExtend pos t qs pps@(pwp, _) = do let vpi = mkId noPosition (mkFString "_handleWeakCtxBitExtend") vp = VPred vpi pwp x <- reducePred [] Nothing vp case x of Just ([vp2], b, us, _) -> -- separated out the matching of vp2 for readability case vp2 of (VPred _ (PredWithPositions p2@(IsIn (Class {name=(CTypeclass cid)}) ts) poss)) | cid == idAdd -> do -- we don't use the reduced preds that came with pwp, -- because the tyvars in it won't match the ones in vp2 reduced_vp2 <- findReducedPreds [] [vp2] let reduced_ps = map toPred $ snd $ headOrErr "handleWeakCtxBitExtend" reduced_vp2 -- now put it together let (qs', t', p2', reduced_ps') = niceTypes (qs, t, p2, reduced_ps) return (Left (pos, EWeakCtxBitExtendNeedsAddCtx (pfpString t') (map pfpString qs') (pfpString p2') (map predToDescr reduced_ps') poss)) k -> return (Right pps) _ -> return (Right pps) -- -------------------- -- (1) A PrimSelectable could fail as weak instead of failed-to-reduce because -- there is a variable in the type. For instance, Vector#(n,Bool) being -- selected and expecting an Integer would fail, but because of "n", it -- is not reported as ctx-reduction but as too-weak. -- -- Other situations we could identify: -- * the array type is a variable (or the left-most constructor is a var), -- in which case we could explain that for []-syntax to be used on a -- parameterized type the proviso PrimSelectable is needed. -- for now, the too-weak error should be sufficient? -- handleWeakCtxPrimSelectable :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxPrimSelectable pos t qs pps@(pwp, _) = do let vpi = mkId noPosition (mkFString "_handleWeakCtxPrimSelectable") vp = VPred vpi pwp case (removePredPositions pwp) of (IsIn c [arr, val]) -> do mesg <- isSelectionResultErr pos vp c arr val case mesg of Nothing -> return (Right pps) Just emsg -> return (Left emsg) p -> internalError ("handleWeakCtxPrimSelectable: Unexpected p: " ++ ppReadable p) isSelectionResultErr :: Position -> VPred -> Class -> Type -> Type -> TI (Maybe EMsg) isSelectionResultErr pos vp@(VPred vpi _) c arr val = do -- create new val variable val_var <- newTVar "isSelectionResultErr (element)" KStar vpi let p' = IsIn c [arr, val_var] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' bound_tyvars <- getBoundTVs case x of -- there is an instance of PrimSelectable for type "arr" Just (_, _, us, _) -> let real_val = (apSub us val_var) in -- compare the return result case (mgu bound_tyvars val real_val) of Nothing -> let (arr', real_val', val') = niceTypes (arr, real_val, val) in return $ Just $ wrongSelectionResultErr pos vp arr' real_val' val' Just s -> return Nothing x -> return Nothing handleWeakCtxPrimUpdateable :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxPrimUpdateable pos t qs pps@(pwp, _) = do let vpi = mkId noPosition (mkFString "_handleWeakCtxPrimUpdateable") vp = VPred vpi pwp case (removePredPositions pwp) of (IsIn c [arr, val]) -> do mesg <- isUpdateArgErr pos vp c arr val case mesg of Nothing -> return (Right pps) Just emsg -> return (Left emsg) p -> internalError ("handleWeakCtxPrimUpdateable: Unexpected p: " ++ ppReadable p) isUpdateArgErr :: Position -> VPred -> Class -> Type -> Type -> TI (Maybe EMsg) isUpdateArgErr pos vp@(VPred vpi _) c arr val = do -- create new val variable val_var <- newTVar "isUpdateArgErr (element)" KStar vpi let p' = IsIn c [arr, val_var] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' bound_tyvars <- getBoundTVs case x of -- there is an instance of PrimUpdateable for type "arr" Just (_, _, us, _) -> let real_val = (apSub us val_var) in -- compare the return result case (mgu bound_tyvars val real_val) of Nothing -> let (arr', real_val', val') = niceTypes (arr, real_val, val) in return $ Just $ wrongUpdateArgErr pos vp arr' real_val' val' Just s -> return Nothing x -> return Nothing handleWeakCtxPrimWriteable :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxPrimWriteable pos t qs pps@(pwp, _) = do let vpi = mkId noPosition (mkFString "_handleWeakCtxUpdateable") vp = VPred vpi pwp case (removePredPositions pwp) of (IsIn c [arr, val]) -> do mesg <- isWriteArgErr pos vp c arr val case mesg of Nothing -> return (Right pps) Just emsg -> return (Left emsg) p -> internalError ("handleWeakCtxPrimWriteable: Unexpected p: " ++ ppReadable p) isWriteArgErr :: Position -> VPred -> Class -> Type -> Type -> TI (Maybe EMsg) isWriteArgErr pos vp@(VPred vpi _) c arr val = do -- create new val variable val_var <- newTVar "isWriteArgErr (element)" KStar vpi let p' = IsIn c [arr, val_var] vp' = VPred vpi (PredWithPositions p' []) x <- reducePred [] Nothing vp' bound_tyvars <- getBoundTVs case x of -- there is an instance of PrimSelectable for type "arr" Just (_, _, us, _) -> let real_val = (apSub us val_var) in -- compare the return result case (mgu bound_tyvars val real_val) of Nothing -> let (arr', real_val', val') = niceTypes (arr, real_val, val) in return $ Just $ wrongWriteArgErr pos vp arr' real_val' val' Just s -> return Nothing x -> return Nothing -- -------------------- handleWeakCtxPrimParam :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxPrimParam pos _ _ (pwp, _) = case pwp of (PredWithPositions (IsIn (Class { }) [userty, _]) poss0) -> do let poss = filterPositions pos poss0 ty_str = pfpString userty let vpi = mkId noPosition (mkFString "_handleWeakCtxPrimParam") vp = VPred vpi pwp x <- reducePred [] Nothing vp case x of Just (vps, _, _, _) -> do let ps = niceTypes (map toPred vps) hasVar = Just $ map pfpString ps return $ Left (pos, ECtxErrPrimParam ty_str poss hasVar) _ -> internalError ("handleWeakCtxPrimParam: reduced") _ -> internalError ("handleWeakCtxPrimParam: wrong number of types") handleWeakCtxPrimPort :: Position -> Type -> [PredWithPositions] -> (PredWithPositions, [Pred]) -> TI (Either EMsg (PredWithPositions, [Pred])) handleWeakCtxPrimPort pos _ _ (pwp, _) = case pwp of (PredWithPositions (IsIn (Class { }) [userty, _]) poss0) -> do let poss = filterPositions pos poss0 ty_str = pfpString userty let vpi = mkId noPosition (mkFString "_handleWeakCtxPrimPort") vp = VPred vpi pwp x <- reducePred [] Nothing vp case x of Just (vps, _, _, _) -> do let ps = niceTypes (map toPred vps) hasVar = Just $ map pfpString ps return $ Left (pos, ECtxErrPrimPort ty_str poss hasVar) _ -> internalError ("handleWeakCtxPrimPort: reduced") _ -> internalError ("handleWeakCtxPrimPort: wrong number of types") -- ======================================================================== -- Contexts with Ambiguous Type Variables -- handleAmbiguousContext :: Position -> [TyVar] -> [VPred] -> TI a handleAmbiguousContext pos amb_vars vps = do -- Remove duplicates and implied predicates vps' <- removeImpliedPreds [] [] vps -- produce a list of pairs of ambiguous vars -- and the preds they appear in let findPreds ps v = (v, filter (elem v . tv) ps) let pairs :: [(TyVar, [VPred])] pairs = map (findPreds vps') amb_vars -- use a heuristic to remove ambiguous variables that would be -- determined if other ambiguous variables were resolved first let pairs_minusFD = removeFD pairs let emsg = ambiguousVarsErr pos pairs_minusFD -- Report ambiguous vars on all the contexts. err emsg removeFD :: [(TyVar, [VPred])] -> [(TyVar, [VPred])] removeFD pairs0 = let vset0 = S.fromList (map fst pairs0) foldFn (v, ps) (vset, pairs) = if isDetermined v ps vset then (S.delete v vset, pairs) else (vset, ((v, ps) : pairs)) isDetermined v ps vset = let -- try one dependency tryOneDep ts bs = let dependee_exprs = (boolCompress (map not bs) ts) dependee_vars = tv dependee_exprs dependent_exprs = (boolCompress bs ts) dependent_vars = tv dependent_exprs in (v `elem` dependent_vars) && -- XXX should we rule out when dependee set is null? all (`S.member` vset) dependee_vars -- try all dependencies for a pred anyDep vp = let (IsIn c ts) = toPred vp in any (tryOneDep ts) (funDeps c) in -- if the type is determined in all preds (by any one fundep) all (anyDep) ps in snd $ foldr foldFn (vset0, []) pairs0 -- -------------------- ambiguousVarsErr :: Position -> [(TyVar, [VPred])] -> EMsg ambiguousVarsErr pos pairs = let niceTypesPairs xs = let -- TyVar is not in Types, so have to add TVar constructor upgradeTyVar (v, ps) = (TVar v, ps) -- and then strip it off downgradeTyVar (t, ps) = case t of TVar v -> (v, ps) _ -> internalError ("downgradeTyVar: not TVar") in map downgradeTyVar (niceTypes (map upgradeTyVar xs)) mkVarInfo (v, ps) = let pwps = map toPredWithPositions ps v_str = pfpString v v_pos = getPosition v use_explanations = map mkAmbVarExplanation pwps in (v_str, v_pos, use_explanations) nice_pairs = niceTypesPairs pairs in (pos, EAmbiguous (map mkVarInfo nice_pairs)) mkAmbVarExplanation :: PredWithPositions -> Doc mkAmbVarExplanation (PredWithPositions p@(IsIn c _) poss) = let cid = typeclassId $ name c use_poss_doc = nest 2 (vcat (map (text . prPosition) (nub poss))) use_doc | cid == idBitwise = s2par ("Bitwise operators" ++ " in or at the following locations:") | cid == idBitReduce = s2par ("Bit reduction operator" ++ " in or at the following locations:") | cid == idBits = s2par ("Bits#() proviso introduced" ++ " (for bit vector packing/unpacking)" ++ " in or at the following locations:") | cid == idBitExtend = s2par ("Bit vector extend or truncate" ++ " in or at the following locations:") | cid == idPrimSelectable = s2par ("Selection with []" ++ " in or at the following locations:") | cid == idPrimIndex = -- this shouldn't happen? -- unless we change "<<" and "[x:y]" to take index types? s2par ("Indexing into a vector" ++ " in or at the following locations:") | cid == idEq = s2par ("Equality or inequality operator" ++ " in or at the following locations:") | cid == idLiteral = s2par ("Numeric constant" ++ " in or at the following locations:") | cid == idSizedLiteral = s2par ("Sized numeric constant" ++ " in or at the following locations:") | cid == idRealLiteral = s2par ("Real numeric constant" ++ " in or at the following locations:") | cid == idStringLiteral = s2par ("String constant" ++ " in or at the following locations:") | cid == idArith = s2par ("Arithmetic operator" ++ " in or at the following locations:") | cid == idOrd = s2par ("Comparison operator" ++ " in or at the following locations:") | cid == idBounded = s2par ("Use of minBound or maxBound" ++ " in or at the following locations:") | cid == idPrimParam = s2par ("Assignment to an imported module parameter" ++ " in or at the following locations:") | cid == idPrimPort = s2par ("Assignment to an imported module port" ++ " in or at the following locations:") | otherwise = -- just display the predicate s2par ("The proviso " ++ pfpString p ++ " introduced" ++ " in or at the following locations:") in use_doc $$ use_poss_doc -- ======================================================================== -- Utilities -- removed positions that are the same as the reported position -- and which are otherwise unhelpful filterPositions :: Position -> [Position] -> [Position] filterPositions pos poss = filter (/= noPosition) $ filter (/= pos) poss -- -------------------- -- Given a list of predicates, this returns a subset of the predicates -- which would be sufficient to satisfy the entire set. removeImpliedPreds :: [VPred] -> [Pred] -> [VPred] -> TI [VPred] removeImpliedPreds qs ds [] = return [] removeImpliedPreds qs ds vps = do eps <- mapM (mkEPred . toPred) vps eds <- mapM mkEPred ds eqs <- mapM (mkEPred . toPred) qs (vps',_) <- removeImpliedPreds' ([],eds ++ eqs) (vps,eps) return vps' removeImpliedPreds' :: ([VPred],[EPred]) -> ([VPred],[EPred]) -> TI ([VPred],[EPred]) removeImpliedPreds' keeps ([], []) = return keeps removeImpliedPreds' (keep_vps, keep_eps) ((vp:vps), (ep:eps)) = do bvs <- getBoundTVs let all_bvs = (tv (keep_eps ++ eps)) ++ bvs closed_bvs = closeFD (vp:vps) all_bvs (vp', _) <- satisfyFV closed_bvs (keep_eps ++ eps) [vp] case (vp') of [] -> removeImpliedPreds' (keep_vps, keep_eps) (vps, eps) _ -> removeImpliedPreds' (vp:keep_vps, ep:keep_eps) (vps, eps) removeImpliedPreds' _ _ = internalError "ContextErrors.removeImpliedPreds'" -- Context Too Weak errors only have PredWithPositions removeImpliedPredWPs :: [PredWithPositions] -> [Pred] -> [PredWithPositions] -> TI [PredWithPositions] removeImpliedPredWPs qpwps ds pwps = do vps <- concatMapM mkVPredNoNewPos pwps qps <- concatMapM mkVPredNoNewPos qpwps vps' <- removeImpliedPreds qps ds vps return (map toPredWithPositions vps') -- -------------------- -- In some cases, we want to reduce a pred to its unsatisfiable requirements. -- For instance, if Bits#(Vector#(8,Integer),sz) is not satisfied, we want -- to discover that it is because Bits#(Integer),sz2) could not be satisfied. findReducedPreds :: [Pred] -> [VPred] -> TI [(VPred, [VPred])] findReducedPreds ds vps = do eps <- getTopExplPreds eds <- mapM mkEPred ds bvs <- getBoundTVs let reduceOne vp = do let dvs = (tv vp) ++ bvs (reduce_res, _, _) <- reducePredsAggressive (Just dvs) (eds ++ eps) [vp] case (reduce_res) of -- shouldn't reduce away entirely [] -> internalError ("findReducedPreds: reduces: " ++ ppReadable vp) -- didn't reduce at all [vp'] | toPred vp' == toPred vp -> return (vp, []) -- reduced to other preds ps -> return (vp, ps) mapM reduceOne vps -- Context Too Weak errors only have PredWithPositions findReducedPredWPs :: [Pred] -> [PredWithPositions] -> TI [(PredWithPositions, [Pred])] findReducedPredWPs ds pwps = do vps <- concatMapM mkVPredNoNewPos pwps vps' <- findReducedPreds ds vps let fn (p,ps) = (toPredWithPositions p, map toPred ps) return (map fn vps') -- -------------------- pwpClassIs :: CTypeclass -> PredWithPositions -> Bool pwpClassIs cid1 (PredWithPositions (IsIn c@(Class { name=cid2 }) _) _) | cid1 == cid2 = True pwpClassIs _ _ = False vpClassIs :: CTypeclass -> VPred -> Bool vpClassIs cid (VPred _ pwp) = pwpClassIs cid pwp {- pwpGetTypes :: PredWithPositions -> [Type] pwpGetTypes (PredWithPositions (IsIn _ ts) _) = ts vpGetTypes :: VPred -> [Type] vpGetTypes (VPred _ pwp) = pwpGetTypes pwp -} -- ======================================================================== -- During typecheck, in places where new contexts are deduced, we should -- call this function to propagate fundeps in the substitution and to -- error early on any non-reducible predicates. -- It returns the predicates with the substitution applied -- in case this -- saves effort later of not having to re-apply the substitution so much. updateContexts :: Position -> [VPred] -> TI [VPred] updateContexts pos ps = do -- this will get the subst and apply it to ps (ps', ps_unsat) <- propagateFunDeps ps -- this doesn't need to subst because the preds already have that done _ <- earlyContextReduction pos ps_unsat return ps' -- function to error early if any contexts are not resolvable -- (This function assumes that the substitution has already been applied -- to the predicates.) earlyContextReduction :: Position -> [VPred] -> TI () earlyContextReduction pos ps = do let try_pred p = do isReducible <- isReduciblePred p return (p, isReducible) rs <- mapM try_pred ps let err_preds = map fst (filter (not . snd) rs) when (not (null err_preds)) $ handleContextReduction pos err_preds -- ======================================================================== -- Display a proviso as a string, except for primitive classes which are -- expressed in natural language predToDescr :: Pred -> String predToDescr p@(IsIn (Class { name = CTypeclass cid }) ts) -- primitive classes which users don't know about | cid == idNumEq = case ts of [t1, t2] -> "type " ++ quote (pfpString t1) ++ " and type " ++ quote (pfpString t2) ++ " are equal" _ -> internalError ("predToDescr: " ++ "NumEq instance contains wrong number of types") | cid == idPrimSelectable = case ts of [arr, val] -> "Selection with [] from a value of type " ++ quote (pfpString arr) ++ " results in a value of type " ++ quote (pfpString val) _ -> internalError ("predToDescr: " ++ "PrimSelectable instance contains wrong number of types") | cid == idPrimUpdateable = case ts of [arr, val] -> "A value of type " ++ quote (pfpString arr) ++ " can be updated at compile-time with [] and = " ++ "with an argument of type " ++ quote (pfpString val) _ -> internalError ("predToDescr: " ++ "PrimUpdateable instance contains wrong number of types") | cid == idPrimWriteable = case ts of [arr, val] -> "A value of type " ++ quote (pfpString arr) ++ " can be updated at run-time with [] and <= " ++ " with an argument of type " ++ quote (pfpString val) _ -> internalError ("predToDescr: " ++ "PrimWriteable instance contains wrong number of types") | cid == idPrimIndex = case ts of [ix, sz] -> "Selection with [] is possible with an index value " ++ "of type " ++ quote (pfpString ix) _ -> internalError ("predToDescr: " ++ "PrimIndex instance contains wrong number of types") -- The rest are documented, so it's OK to reveal to the user | otherwise = pfpString p {- | cid == idIsModule = | cid == idBitExtend = | cid == idBitwise = | cid == idBitReduce = | cid == idSizedLiteral = | cid == idLiteral = | cid == idRealLiteral = | cid == idStringLiteral = -} -- ========================================================================