{-# LANGUAGE PatternGuards #-} module TCMisc( splitF, satisfyFV, satisfy, reducePred, reducePredsAggressive, expPrimTCons, expTConPred, findAssump, mkQualType, closeFD, niceTypes, unifyFnFrom, unifyFnTo, unifyFnFromTo, mkSchemeNoBVs, rmPatLit, rmQualLit, expandSynN, expandFullType, unify, unifyNoEq, mkVPred, mkVPredNoNewPos, mkVPredFromPred, toPredWithPositions, toPred, defaultClasses, checkForAmbiguousPreds, propagateFunDeps, isReduciblePred ) where import Data.Maybe import Data.List import Control.Monad(foldM, when) import qualified Data.Map as M import qualified Data.Set as S import System.IO.Unsafe(unsafePerformIO) import ListMap(lookupWithDefault) import Util import PFPrint import Position import CType import FStringCompat(mkFString) import Id import Error(internalError, EMsg, ErrMsg(..)) import Flags(Flags, useProvisoSAT) import Type import Subst import Assump import Scheme import Unify import Pred import SATPred import TIMonad import PreIds import StdPrel(isPreClass) import CSyntax(CDefl(..), CExpr(..), CPat(..), CQual(..), CLiteral(..), cTApply, cVApply, anyTExpr) import Literal import IntLit import SymTab import MakeSymTab(convCQType) import PreStrings(sAcute) import IOUtil(progArgs) import Debug.Trace ------- doRTrace :: Bool doRTrace = elem "-trace-type" progArgs rtrace :: String -> a -> a rtrace s x = if doRTrace then traces s x else x doTraceSatisfy :: Bool doTraceSatisfy = elem "-trace-tc-satisfy" progArgs satTrace :: String -> a -> a satTrace s x = if doTraceSatisfy then traces s x else x satTraceM :: Monad m => String -> m () satTraceM s = when (doTraceSatisfy) $ traceM s doTraceReducePred :: Bool doTraceReducePred = elem "-trace-tc-reducepred" progArgs rpTrace :: String -> a -> a rpTrace s x = if doTraceReducePred then traces s x else x doVarTrace :: Bool doVarTrace = elem "-trace-tcvar" progArgs ------- type DVS = Maybe [TyVar] splitF :: [TyVar] -> [VPred] -> ([VPred], [VPred]) splitF fs ps = partition (all (`elem` fs) . tv) ps ------- -- The following "satisfy" functions take a list of predicates -- ("es" of type [EPred]) which can be assumed to exist (that is, they -- are the provided context in an explicitly-typed let-binding, and -- the converted function will take in dictionaries for these -- predicates). And they take a list of predicates which were -- inferred, and need to be solved. And they return a list of any -- unsolved predicates, and new definitions for dictionaries of any -- predicates which were solved. (The dictionaries are defined in -- terms of existing dictionaries, such as the "es".) satisfy :: [EPred] -> [VPred] -> TI ([VPred], [CDefl]) satisfy es ps = satisfyX Nothing es ps -- This version also takes a list of the variables from the -- environment, which have been filtered for dependencies. These -- TyVars are used only in "genInsts" (in "reducePred") for numeric -- classes in the StdPrel. For example (Add x y (TVar v)) only turns -- into (Add x y (TAdd x y)) if the "v" being replaced isn't in the -- list of TyVars. satisfyFV :: [TyVar] -> [EPred] -> [VPred] -> TI ([VPred], [CDefl]) satisfyFV vs es ps = satTrace ("satisfyFV " ++ ppReadable ps) $ satisfyX (Just vs) es ps satisfyX :: DVS -> [EPred] -> [VPred] -> TI ([VPred], [CDefl]) satisfyX _ es [] = return ([], []) satisfyX dvs es ps = do -- satTraceM ("satisfy enter: " ++ ppString (dvs, ps)) -- it is not clear if applying the substitution here wins or not s0 <- getSubst (rs, bs, s) <- satisfy' dvs (apSub s0 es) (apSub s0 ps) -- (rs, bs, s) <- satisfy' dvs es ps -- satTraceM ("satisfy exit: " ++ ppString (rs,bs,s) ++ "\n") extSubst "satisfyX" s return $ (rs, apSub s (map mkDefl bs)) -- break up preds into those affected by a substitution and those not -- in order to loop more efficiently in satisfy' split_rs :: Subst -> [VPred] -> ([VPred], [VPred]) split_rs s' rs = partition affected_pred rs -- should only be a few since classes are small -- and the substitution comes from a single reducePred -- or joinCtx (at the end) where changed_tv = getSubstDomain s' affected_var v = v `elem` changed_tv affected_pred r = any affected_var (tv r) satisfy' :: DVS -> [EPred] -> [VPred] -> TI ([VPred], [Bind], Subst) satisfy' dvs es ps = do (ps0, s0, bs0) <- joinNeededCtxs ps -- satTraceM ("satisfy (join)' = " ++ ppString (ps0, bs0, s0)) (vp, binds, s) <- sMany dvs es [] bs0 s0 ps0 -- satTraceM ("satisfy (result)' = " ++ ppString (vp,binds,s)) return (vp, binds, s) where -- sMany -- Arguments: -- dvs - dependent vars, when attempting "last resort" satisfying -- es - given preds, which can be assumed for satisfying other preds -- rs - preds which we tried to satisfy but couldn't -- bs - bindings resulting from satisfying -- s - substitution resulting from satisfying -- ps - the predicates to try satisfying -- Try satisfying each pred in "ps" in turn. If "sat" cannot reduce -- it entirely (that is, "sat" returns the preds that it reduced to), -- then we ignore the result of "sat" and put the predicate aside -- (in "rs"). If "sat" can reduce the pred entirely, then we add the -- pred to the list of known preds ("es") and we add the bindings -- and substitution to the current result. If the subst gives us -- new information about any of the unsatisfied preds ("rs") then -- we attempt to solve those again (put them back in "ps") in case -- progress can be made with the new information. -- -- XXX Why do we ignore the result when a pred doesn't sat all the way? -- Is it for better error messages? That is, so that we report the -- original pred? -- XXX Can we at least keep any of the substitution? -- -- Note that we do allow partial results from numeric typeclasses -- (but only when not attempting "last resort" satisfying, though -- is that condition even necessary?). -- sMany :: DVS -> [EPred] -> [VPred] -> [Bind] -> Subst -> [VPred] -> TI ([VPred], [Bind], Subst) sMany dvs es rs bs s [] = {- satTrace ("sMany: rs=" ++ ppReadable rs) $ -} do (rs', s', bs') <- joinNeededCtxs rs let (changed_rs, unchanged_rs) = split_rs s' rs' if null changed_rs then do checkJoinCtxs "satisfy" rs s' rs' return (rs', bs' ++ bs, s' @@ s) else sMany (dvsSub s' dvs) (apSub s' es) unchanged_rs (bs' ++ bs) (s' @@ s) (apSub s' changed_rs) sMany dvs es rs bs s (p:ps) = do x <- sat dvs es p -- satTrace ("sMany: sat=" ++ ppReadable (p, x)) $ return () case x of -- if the predicate failed to reduce away completely, -- put it aside and ignore its result, -- except when it's a numeric typeclass and we're not doing -- "last resort" satisfying ((_:_), _, _) | not (vpIsPreClass p) || isJust dvs -> sMany dvs es (p:rs) bs s ps (new_ps, bs', s') -> if isNullSubst s' then sMany dvs es (new_ps ++ rs) (bs'++bs) s ps else do let (changed_rs, unchanged_rs) = split_rs s' rs sMany (dvsSub s' dvs) (apSub s' es) (new_ps ++ unchanged_rs) (bs' ++ bs) (s' @@ s) (apSub s' (changed_rs ++ ps)) expTConPred :: VPred -> TI [VPred] expTConPred (VPred e (PredWithPositions (IsIn c ts) pos)) = do vsts <- mapM expPrimTCons ts let (vss, ts') = unzip vsts return (VPred e (PredWithPositions (IsIn c ts') pos): concat vss) primTConMap :: [(Id, Id -> Type -> TI ([VPred], Type))] primTConMap = [(idSizeOf, expSizeOfT), (idId, expIdOfT)] -- default action for TCons -- no need to recurse because there is no additional structure defaultTConAp :: Type -> Id -> Type -> TI ([VPred], Type) defaultTConAp tcon _ t = do (ps, t') <- expPrimTCons t return (ps, TAp tcon t') -- expand all primitive type-constructors (SizeOf, Id, ...) expPrimTCons :: Type -> TI ([VPred], Type) expPrimTCons (TAp tcon@(TCon (TyCon idcon _ _)) t) = do -- traceM ("idcon: " ++ ppReadable idcon) let f = lookupWithDefault primTConMap (defaultTConAp tcon) idcon f idcon t expPrimTCons (TAp f a) = do (vfs, f') <- expPrimTCons f (vas, a') <- expPrimTCons a return (vfs++vas, TAp f' a') expPrimTCons t = return ([], t) expSizeOfT :: Id -> Type -> TI ([VPred], Type) expSizeOfT sz t = do v <- newTVar "expSizeOfT" KNum sz bits <- bitCls vp <- mkVPredFromPred [getPosition sz] (IsIn bits [t, v]) return ([vp], v) -- eliminate the identity type constructior expIdOfT :: Id -> Type -> TI ([VPred], Type) expIdOfT _ t = do -- traceM ("expIdOf: " ++ ppReadable t) return ([], t) -- This is faster than the old joinCtxs in the pathological case -- where no contexts are found because we discover that with -- an O (n log n) sort, instead of an O(n^2) scan -- We sort by the class, the fundep pattern used and the compressed tyvars -- More complex, so possibly less efficient than scanning -- when a suitable match is found early in the list -- Hopefully a good trade-off -- XXX For efficiency, we should "join in parallel", -- i.e. attempt to merge possible substitutions -- so that we can handle more than one duplicate pred at once joinCtxs :: [TyVar] -> [VPred] -> Maybe ([VPred], Subst, Bind) joinCtxs bound_tyvars vps = listToMaybe (mapMaybe matchBlobs joined_blob_list) where blob_list = [((c, n, boolCompress (map not bs) ts), vp) | vp@(VPred _ (PredWithPositions (IsIn c ts) _)) <- vps, (n, bs) <- zip [0..] (funDeps c)] joined_blob_list = joinByFst blob_list matchPreds n (VPred i pp@(PredWithPositions (IsIn c ts) pos)) (VPred i' pp'@(PredWithPositions (IsIn _ ts') pos')) = do let bs = funDeps c !! n -- we could try to capture and use numeric equalities here -- but that would require being on the TI monad, -- which doesn't seem worth it (s, []) <- mgu bound_tyvars (boolCompress bs ts) (boolCompress bs ts') let p'' = VPred i' (PredWithPositions (IsIn c ts') (pos' ++ pos)) rs = p'':[ vp | vp@(VPred j _) <- vps, j /= i && j /= i'] pr = removePredPositions pp return (rs, s, (i, predToType (apSub s pr), CVar i')) -- uniquePairs because we need to try every possible pair of matching VPreds matchBlobs ((_,n,_), vps) = listToMaybe $ mapMaybe (uncurry (matchPreds n)) $ uniquePairs vps -- This function is successful if the list of VPred is empty, indicating -- that the pred was fully satisfied. In which case, the bindings and subst -- can be used freely. -- If the list of VPred is non-empty, that means that we were able to reduce -- the given VPred to the list of preds, and the bindings indicate how we got -- there. The subst may still be useful b/c it includes what we learned from -- functional dependencies whether or not the VPred is satisfied "all the way" -- -- sat corresponds to section 7.2 "Entailment" in the paper -- Typing Haskell in Haskell sat :: DVS -> [EPred] -> VPred -> TI ([VPred], [Bind], Subst) {- sat dvs ps (VPred w pr@(IsIn bts [t1, TAp szof t2])) | name bts == idBits && szof == tSizeOf = do traces ("SizeOf " ++ ppReadable pr) $ return () tunify t1 t1 t2 -- XXX t1 v <- newTVar KNum szof sat dvs ps (VPred w (IsIn bts [t1, v])) -} sat dvs ps p = satTrace ("sat: trying " ++ ppReadable p ++ " in " ++ ppReadable ps) $ do whole_stack <- getSatStack bound_tyvars <- getBoundTVs let lookfor_result :: Maybe ([Bind], (Subst, [(Type,Type)])) -- I'm a little worried that matching against the whole_stack -- will have lexical scoping issues where p will match against -- something very "old", that it should not be able to "see" -- due to shadowing or something. We are probably OK because -- the TIMonad is reset for each top-level definition. lookfor_result = lookfor bound_tyvars p whole_stack case lookfor_result of Just (bs, (s, [])) -> -- tie the recursive knot! -- traces ("recursive knot: " ++ (ppString p) ++ " = " ++ (ppString lookfor_result))$ case p of (VPred vp (PredWithPositions (IsIn cl tys) poss)) | (name cl) == (CTypeclass idBits) -> err (makeERecursiveBitsErrorMessage poss tys cl) {- internalError ( "cl: " ++ (ppString cl) ++ "\n\ntys: " ++ (ppString tys) ++ "\n\npos: " ++ (ppString pos) ++ "\n\nlf: " ++ (ppString lookfor_result) ++ "\n\nvp: " ++ (ppString vp) ++ "\n\nvp tys: " ++ (pfpString tys) ++ "" ) -} -- if we satisfy numeric provisos recursively, we haven't proven it (VPred vp (PredWithPositions (IsIn cl _) poss)) | isPreClass cl -> return ([p], [], nullSubst) _ -> satTrace ("sat recursive: " ++ ppReadable (p, bs, s)) $ return ([], bs, s) _ -> do let this_point :: TSSatElement this_point = (mkTSSatElement dvs ps p) incrementSatStack this_point return_val <- case lookfor bound_tyvars p (concatMap bySuperE ps) of Just (bs, (s, [])) -> do satTrace ("sat in super: " ++ ppReadable (p, concatMap bySuperE ps)) $ return () return ([], bs, s) -- we might introduce a numeric equality here, so try instance reduction first m_equals -> do -- if instance reduction fails, fall back to introducing an equality let fail msg = case m_equals of Just (bs, (s, num_eqs)) -> do satTrace ("sat in super (num eq): " ++ ppReadable (p, concatMap bySuperE ps, num_eqs)) $ return () eq_ps <- mapM (eqToVPred (getVPredPositions p)) num_eqs satMany (dvsSub s dvs) (apSub s ps) [] bs s eq_ps Nothing -> satTrace msg $ return ([p], [], nullSubst) ai <- getAllowIncoherent x <- reducePred ps dvs p case x of Nothing -> fail "sat unreduced" Just (qs, b, us, Nothing) -> satTrace ("sat calls satMany ") $ do satMany (dvsSub us dvs) (apSub us ps) [] [b] us qs -- qs should have us applied already Just (qs, b, us, Just (h@(IsIn c _))) | fromMaybe ai (allowIncoherent c) -> satTrace ("sat calls satMany (incoherent) ") $ do result <- satMany (dvsSub us dvs) (apSub us ps) [] [b] us qs case result of (ps@(_:_), bs, s_final) -> return $ (ps, bs, s_final) ([], bs, s_final) -> do let (vp_pred, inst_pred) = niceTypes (apSub s_final (toPred p, h)) let pos = getPosition $ getVPredPositions p when (allowIncoherent c /= Just True) $ twarn (pos, WIncoherentMatch (pfpString vp_pred) (pfpString inst_pred)) return $ ([], bs, s_final) bad_match -> fail ("sat incoherent disallowed: " ++ ppReadable bad_match) decrementSatStack return return_val makeERecursiveBitsErrorMessage :: [Position] -> [Type] -> Class -> EMsg -- a somewhat hacky function which tries to come up with the best -- error message possible makeERecursiveBitsErrorMessage poss tys cl = let remove_tyvars :: Type -> Bool -- often TVars are compiler generated and not useful. remove_tyvars (TVar _) = False remove_tyvars _ = True in ((case poss of [] -> noPosition -- first position seems as good as any pos1:_ -> pos1 ), (ERecursiveBits (pfpString (name cl)) (case (filter remove_tyvars tys) of [] -> pfpString tys [singleton] -> pfpString singleton list -> pfpString list) )) -- make sure we've joined contexts "all the way" checkJoinCtxs :: String -> [VPred] -> Subst -> [VPred] -> TI () checkJoinCtxs tag rs s rs' = do bound_tyvars <- getBoundTVs when (isJust (joinCtxs bound_tyvars rs')) $ internalError ("incomplete join (" ++ tag ++ "): " ++ ppReadable (rs, rs', s)) joinNeededCtxs :: [VPred] -> TI ([VPred], Subst, [Bind]) joinNeededCtxs = joinNeededCtxs' nullSubst [] joinNeededCtxs' :: Subst -> [Bind] -> [VPred] -> TI ([VPred], Subst, [Bind]) joinNeededCtxs' s bs ps = do bvs <- getBoundTVs case (joinCtxs bvs ps) of Nothing -> return (ps, s, bs) Just (ps', s', b) -> let (changed_rs, unchanged_rs) = split_rs s' ps' rs' = (apSub s' changed_rs) ++ unchanged_rs in joinNeededCtxs' (s' @@ s) (b:bs) rs' -- as we commit to substitutions, we extend the monad with them -- we preserve them this far so we can efficiently decide which -- preds to retry satisfying -- -- Return values are similar to "sat" since they recursively call each other. satMany :: DVS -> [EPred] -> [VPred] -> [Bind] -> Subst -> [VPred] -> TI ([VPred], [Bind], Subst) -- rs_accum is an accumulating parameter of "needed" VPreds -- if satisfying fails these are returned (for error messages and ctxReduce) satMany dvs es [] bs s [] = return $ ([], bs, s) satMany dvs es rs_accum bs s [] = do (final_rs, s', bs') <- joinNeededCtxs rs_accum return $ (final_rs, bs' ++ bs, s' @@ s) satMany dvs es rs_accum bs s (p:ps) = do x <- sat dvs es p rtrace ("satMany: sat="++ ppReadable (p,x)) $ return () case x of (needed@(_:_), bs', s') -> -- If we are unable to satisfy "p", we add the "needed" -- preds to the "rs_accum" argument, potentially heading toward -- the "return Nothing" case above. -- We also accum the bindings to get from "p" to "needed". -- we keep growing the substitution because anything we -- have learned we can commit to rtrace ("satMany Right: " ++ ppReadable needed) $ satMany dvs es (needed ++ rs_accum) (bs'++bs) (s' @@ s) ps ([], bs', s') -> -- If p is satisfied, we "drop" it, but add its binding and -- substitution. if isNullSubst s' then -- Straight-up drop it rtrace ("satMany Left True") $ satMany dvs es rs_accum (bs'++bs) s ps else do let (changed_rs, unchanged_rs) = split_rs s' rs_accum if null changed_rs then -- no impact on accumulated predicates rtrace ("satMany Left False True") $ satMany dvs es rs_accum (bs'++bs) (s' @@ s) (apSub s' ps) else -- Drop it, but try from the beginning again to see if any of -- the accumulated rs's can now be -- satisfied in the New State Of The World. This might lead to -- horrible running time in the worst case. rtrace ("satMany Left False False") $ do let rs' = (apSub s' changed_rs) ++ unchanged_rs (rs'', s1, bs1) <- joinNeededCtxs rs' let s2 = s1 @@ s' satMany (dvsSub s2 dvs) (apSub s2 es) [] (bs1 ++ bs'++ bs) (s2 @@ s) (rs'' ++ apSub s2 ps) -- try to reduce the supplied VPreds as far as possible -- returning the underlying preds required reducePredsAggressive :: DVS -> [EPred] -> [VPred] -> TI ([VPred], [CDefl], Subst) reducePredsAggressive dvs es vps0 = do -- traceM ("reducePredsAggressive (enter): " ++ ppReadable vps0) (vps1, s1, bs1) <- joinNeededCtxs vps0 checkJoinCtxs "reducePredsAggressive 1" vps0 s1 vps1 reducePredsAggressive' dvs es bs1 s1 vps1 reducePredsAggressive' :: DVS -> [EPred] -> [Bind] -> Subst -> [VPred] -> TI ([VPred], [CDefl], Subst) reducePredsAggressive' dvs es bs1 s1 vps1 = do (vps2, bs2, s2) <- maskAllowIncoherent $ satMany dvs es [] [] s1 vps1 checkJoinCtxs "reducePredsAggressive 2" vps1 s2 vps2 let allPredTyCons = concat [ concatMap allTyCons ts | IsIn _ ts <- map toPred vps2 ] let badCon (TyCon _ _ (TItype _ _)) = True badCon (TyCon i _ _) = isJust (lookup i primTConMap) badCon _ = False if (any badCon allPredTyCons) then do -- loop to keep synonyms and SizeOf out of instance heads vps2' <- concatMapM (expTConPred . expandSynVPred) vps2 reducePredsAggressive' dvs es (bs1 ++ bs2) s2 vps2' else do -- satMany is inside a loop, so it doesn't consistently apply -- its accumulated substitution to the reduced predicates. -- Apply the substitution here to clean that up before returning -- to the external caller. return (apSub s2 vps2, map mkDefl (bs1 ++ bs2), s2) -- note that the subst we return is safe to commit to as long as the -- instance match isn't incoherent (or if we are ok committing to an -- incoherent match) reducePred :: [EPred] -> DVS -> VPred -> TI (Maybe ([VPred], Bind, Subst, Maybe Pred)) reducePred eps dvs (VPred w pp@(PredWithPositions pr@(IsIn c ts) pos)) = do pushSatStackContext bound_tyvars <- getBoundTVs ts' <- mapM normT ts let pr' = IsIn c ts' pp' = PredWithPositions pr' pos v' = VPred w pp' f :: Bool -> [Inst] -> TI (Maybe ([VPred], Bind, Subst, Maybe Pred)) f incoherent [] = return Nothing f incoherent (i:is) = do (m_tv, i'@(Inst _ _ (_ :=> h))) <- newInst i (getVPredPositions v') x <- byInst v' i' case x of Nothing -> do let chk = predUnify bound_tyvars pr' h f (chk || incoherent) is Just (qs, b, (inst_subst, fd_subst)) -> do -- when ((not $ null qs) && (not $ isNullSubst inst_subst)) $ -- traceM("qs, inst_subst, fd_subst: " ++ ppReadable (qs, inst_subst, fd_subst)) -- does the inst_subst affect anything *outside* of the instance? let bad_inst_subst = fromMaybe inst_subst $ fmap (flip trimSubst $ inst_subst) m_tv when (not (isNullSubst bad_inst_subst)) $ internalError("reducePred - bad inst subst: " ++ ppReadable (v', i', m_tv, inst_subst, fd_subst, incoherent)) let Inst _ _ (_ :=> h) = i let minst = toMaybe incoherent h return $ Just (qs,b,fd_subst,minst) let is' = genInsts c bound_tyvars dvs pr' r <- f False is' rpTrace ("reducePred " ++ ppReadable (dvs, pr', is', r)) $ return () popSatStackContext flags <- getFlags if (useProvisoSAT flags) && (isNothing r) && (isPreClass c) then do --traceM("attempting to solve numeric proviso") let ps = [ p | (EPred _ p) <- eps ] let res = unsafePerformIO $ do s <- initSATPredState flags (r, _) <- solvePred s ps pr' return r case res of Nothing -> do --traceM(" failed.") return Nothing Just _ -> do -- XXX for now, no new info is learned, just sat --traceM(" success.") let r = anyTExpr (predToType pr') let b = (w, predToType pr', r) return $ Just ([], b, nullSubst, Nothing) else return r predUnify :: [TyVar] -> Pred -> Pred -> Bool predUnify bound_tyvars (IsIn c1 ts1) (IsIn c2 ts2) | c1 == c2 = isJust (mgu bound_tyvars ts1 ts2) | otherwise = False dvsSub :: Subst -> DVS -> DVS dvsSub s dvs = dvs {- dvsSub _ Nothing = Nothing dvsSub s dvs = if isNullSubst s then dvs else traces ("dvsSub " ++ ppReadable (dvs, s)) dvs -} byInst :: VPred -> Inst -> TI (Maybe ([VPred], Bind, (Subst, Subst))) byInst (VPred i p) (Inst e _ (ps :=> h)) = do -- no longer necessary because reducePred now provides a fresh instance -- Inst e _ (ps :=> h) <- newInst ii (getPredPositions p) bound_tyvars <- getBoundTVs let m = matchTop bound_tyvars matchList h (removePredPositions p) -- rtrace ("byInst " ++ ppReadable (p, ps :=> h, m)) $ return () case m of Nothing -> return Nothing Just (inst_subst, (fd_subst, num_eqs)) -> do let s = fd_subst @@ inst_subst vs <- mapM (const newDict) ps -- if the instance is recursive (has a proviso for itself and expects -- a dictionary argument for that), then don't use a new dictionary -- for that argument, just pass the instance to itself let vs' = zipWith (\ x y -> if (y == p) then i else x) vs (apSub s ps) eq_ps <- mapM eqToPred num_eqs let eq_pwps = map (mkPredWithPositions []) eq_ps eq_vs <- mapM (const newDict) eq_pwps -- if p introduces a new predicate, carry on the position info let mkvpred x y = VPred x (addPredPositions y (getPredPositions p)) -- if the instance is recursive one of these will be unused? ps' = zipWith mkvpred (vs ++ eq_vs) (map (apSub s) (ps ++ eq_pwps)) t = predToType (apSub s h) e' = apSub s e ps'' <- concatMapM (expTConPred . expandSynVPred) ps' -- rtrace ("byInst: " ++ ppReadable (ps', e', t)) $ return () return (Just (ps'', (i, t, CApply e' (map CVar vs')), (inst_subst, fd_subst))) -- Create a new instance by replacing the type variables in the instance -- with fresh variables. -- Give the variables a position based on where the predicate was -- introduced (the list of positions is the positions where the predicate -- was introduced). XXX unfortunately we can only pass one pos to the var -- Also the lowest TVar, for use in trimming newInst :: Inst -> [Position] -> TI (Maybe TyVar, Inst) newInst ii@(Inst _ vs _) poss = do let getpos v = getMostUsefulPosition poss (getPosition v) when doVarTrace $ traceM ("newInst " ++ ppReadable ii) ts <- mapM (\ v -> newTVar "newInst" (kind v) (getpos v)) vs let v = case ts of (TVar x:xs) -> Just x _ -> Nothing return (v, apSub (mkSubst (zip vs ts)) ii) lookfor :: [TyVar] -> VPred -> [EPred] -> Maybe ([Bind], (Subst, [(Type, Type)])) lookfor bound_tyvars _ [] = Nothing lookfor bound_tyvars v@(VPred i pp) eps@(EPred e pr':ps) = let pr = removePredPositions pp meq x y = if x == y then Just nullSubst else Nothing in -- traces ("lookfor " ++ ppReadable (pr, pr', matchTop bound_tyvars meq pr pr', ps)) $ case matchTop bound_tyvars meq pr pr' of Just (inst_subst, fd_subst_and_eqs) | isNullSubst inst_subst -> Just ([(i, predToType pr, e)], fd_subst_and_eqs) Just (inst_subst, fd_subst) -> internalError ("lookfor bad: " ++ ppReadable (bound_tyvars, v, eps, inst_subst, fd_subst)) Nothing -> lookfor bound_tyvars v ps commute :: [Type] -> [Type] commute ts@[t1,t2] = [t2, t1] commute ts@[t1,t2,t3] = [t2, t1, t3] commute _ = internalError("commutative class not taking two or three arguments") bySuperE :: EPred -> [EPred] bySuperE ep@(EPred e p@(IsIn c ts)) = ep : eps ++ comm where s = mkSubst (zip (csig c) ts) esupers = map (\ (CTypeclass i, p) -> let p' = apSub s p in EPred (CApply (cTApply (CSelectT (typeclassId $ name c) i) ts) [e]) p') (super c) eps = concatMap bySuperE esupers comm = if (isComm c) then {- (traces ("expr: " ++ ppReadable e) $-} [(EPred e (IsIn c (commute ts)))] else [] -- Given: -- * bound variables -- * a function for determining when two predicates "match" -- (by matching their lists of type parameters) -- which returns the substitution which makes them match -- * two predicates -- Returns: -- * two substitutions: -- the first is applied to the instance (to specialize it) -- the second is anything we've learned from fundeps (added to the monad) -- the second substitution is paired with any numeric equalities we discover -- we need -- -- This function is used by byInst to test if a predicate matches an instance, -- where the "match" function is list unification. By changing the match -- function, this could be used in other ways. -- matchTop :: [TyVar] -> ([Type] -> [Type] -> Maybe Subst) -> Pred -> Pred -> Maybe (Subst, (Subst, [(Type, Type)])) matchTop bound_tyvars mtch (IsIn c1 ts1) (IsIn c2 ts2) = -- rtrace ("matchTop: " ++ ppReadable (IsIn c1 ts1, IsIn c2 ts2, c1==c2)) $ if c1 /= c2 then -- different classes obviously don't match Nothing else -- rtrace ("matchTop 0: " ++ ppReadable (name c1, funDeps c1, ts1, ts2)) $ let mfd bs = -- first check that the nonfundep types match let nbs = map not bs v1 = (boolCompress nbs ts1) v2 = (boolCompress nbs ts2) mv = mtch v1 v2 in case mv of Nothing -> -- rtrace ("matchTop 1a: " ++ ppReadable (v1, v2, mv)) $ Nothing Just ms -> -- if the nonfundep types match, then apply the found -- substitution and see if the fundep types match -- rtrace ("matchTop 1b: " ++ ppReadable ms) $ case mgu bound_tyvars (apSub ms (boolCompress bs ts1)) (apSub ms (boolCompress bs ts2)) of Nothing -> Nothing Just us -> Just (ms, us) in -- find the first fundep list which matches -- XXX the fundep lists are not used jointly? pickJust (map mfd (funDeps c1)) pickJust :: [Maybe a] -> Maybe a pickJust mxs = foldr pickL Nothing mxs where pickL m@(Just _) _ = m pickL _ m = m ------- findAssump :: Id -> [Assump] -> TI Assump findAssump i as = case [ sc | (i':>:sc) <- as, i==i' ] of [] -> do s <- getSymTab case findVar s i of Nothing -> errorAtId EUnboundVar i Just (VarInfo _ a d) -> do case d of Nothing -> return () Just str -> twarn (getPosition i, WDeprecated "definition" (pfpString i) str) return (updAssumpPos i a) sc : _ -> return (i :>: sc) ------- mkSchemeNoBVs :: CQType -> TI Scheme mkSchemeNoBVs cqt = do sy <- getSymTab bvs <- getBoundTVs case convCQType sy cqt of Left emsg -> err emsg Right qt -> return (quantify (tv qt \\ bvs) qt) mkQualType :: CQType -> TI (Qual Type) mkQualType cqt = do s <- getSymTab case convCQType s cqt of Left emsg -> err emsg Right qt -> return qt ------- rmPatLit :: CPat -> TI (CPat, [CQual]) --rmPatLit p = return (p, []) rmPatLit (CPCon i ps) = do pqs <- mapM rmPatLit ps let (ps', qss) = unzip pqs return (CPCon i ps', concat qss) rmPatLit (CPstruct mb i ips) = do let f (i, p) = do (p, qs) <- rmPatLit p; return ((i, p), qs) ipqs <- mapM f ips let (ips', qss) = unzip ipqs return (CPstruct mb i ips', concat qss) rmPatLit p@(CPVar _) = return (p, []) rmPatLit (CPAs i p) = do (p', qs) <- rmPatLit p return (CPAs i p', qs) rmPatLit p@(CPAny {}) = return (p, []) rmPatLit (CPLit (CLiteral p l)) = do v <- newVar p "rmPatLit" return (CPVar v, [CQFilter (cVApply idEqual [CVar v, CLit (CLiteral p l)])]) rmPatLit (CPMixedLit pos base ps) = do -- only binary, hex and octal are legal let bitwidth = log2 base v <- newVar pos "rmPatLit" let mkLit len val = CLit (CLiteral pos (LInt (IntLit { ilWidth = Just len, ilBase = base, ilValue = val }))) mkUnsizedLit val = CLit (CLiteral pos (LInt (ilDec val))) let foldfunc (len, Nothing) (idx, quals) = (idx + (len * bitwidth), quals) foldfunc (len, Just val) (idx, quals) = let bitsize = len * bitwidth lo = mkUnsizedLit idx hi = mkUnsizedLit (idx + bitsize - 1) extract_expr = CSub2 (CVar v) hi lo val_expr = mkLit bitsize val q = CQFilter (cVApply idEqual [extract_expr, val_expr]) in (idx + bitsize, q:quals) (_, quals) = foldr foldfunc (0,[]) ps return (CPVar v, quals) rmPatLit (CPCon1 ti i p) = do (p', qs) <- rmPatLit p return (CPCon1 ti i p', qs) rmPatLit (CPConTs ti i ts ps) = do pqs <- mapM rmPatLit ps let (ps', qss) = unzip pqs return (CPConTs ti i ts ps', concat qss) rmPatLit _ = internalError "TCMisc.rmPatLit" rmQualLit :: CQual -> TI [CQual] rmQualLit q@(CQFilter _) = return [q] rmQualLit (CQGen i p e) = do (p', qs) <- rmPatLit p return (CQGen i p' e : qs) ------- -- only for expanding synonyms when you are NOT on a type-checking monad -- will substitute in fresh variables for all type variables in the input type -- to avoid variable capture expandSynN :: Flags -> SymTab -> Type -> Type expandSynN flags s t = -- should only need to match instances for coherent typeclasses -- XXX user code corner-case? case fst $ runTI flags False s $ do addBoundTVs (tv t) -- to prevent generated variable capture normT t of Left msg -> internalError ("expandSynN " ++ ppReadable msg) Right t -> t normT :: Type -> TI Type normT t = do let t' = expandSyn t (ps, t'') <- expPrimTCons t' -- traceM ("normT: " ++ ppReadable (t,t',(ps,t''))) if null ps then return t'' else do (ps', _) <- satisfy [] ps --unless (null ps') (internalError ("expandSynN " ++ ppReadable (t, ps'))) if not (null ps') then return t' -- XXX could expand some else do s <- getSubst let t''' = expandSyn (apSub s t'') --traces ("normT " ++ ppReadable (ps', t''', s)) $ return () return t''' -- expands synonyms and applies the substitution -- to get a "fully desugared" type based on all -- available information expandFullType :: Type -> TI (Type) expandFullType t = do sy <- getSymTab s <- getSubst tunexp <- normT t let t' = expandSyn (apSub s tunexp) return (t') ---- -- a::x is only used for error reporting unify :: (PPrint a, PVPrint a, HasPosition a) => a -> Type -> Type -> TI ([VPred]) unify x t1 t2 = do let pos = getPosition x -- traceM("unify 1: " ++ ppReadable(t1, t2)) s <- getSubst bound_vars <- getBoundTVs let t1' = apSub s t1 t2' = apSub s t2 -- traceM("unify 2: " ++ ppReadable(t1', t2')) case mgu bound_vars t1' t2' of Just (u,[]) -> do extSubst "unify" u; return [] otherwise -> do t1'' <- normT t1' t2'' <- normT t2' -- traceM ("unify 3:\n" ++ ppReadable (t1'', t2'')) case mgu bound_vars t1'' t2'' of Just (u,eqs) -> do extSubst "unify" u mapM (eqToVPred [pos]) eqs Nothing -> let (t1'', t2'') = niceTypes (t1', t2') in reportUnifyError bound_vars x t1'' t2'' eqToPred :: (Type, Type) -> TI Pred eqToPred (t1, t2) = do clsNumEq <- numEqCls return $ IsIn clsNumEq [t1, t2] eqToVPred :: [Position] -> (Type, Type) -> TI VPred eqToVPred poss num_eq = do p <- eqToPred num_eq mkVPredFromPred poss p unifyNoEq :: (PPrint a, PVPrint a, HasPosition a) => [Char] -> a -> Type -> Type -> TI () unifyNoEq loc x t1 t2 = do ps <- unify x t1 t2 when (not $ null ps) $ internalError ("unexpected unification equalities (" ++ loc ++ "): " ++ ppReadable(t1, t2, ps)) return () ----- reportUnifyError :: (PPrint a, PVPrint a, HasPosition a) => [TyVar] -> a -> Type -> Type -> TI b reportUnifyError bound_vars x orig_t1 orig_t2 = let def_err = defaultUnifyError x orig_t1 orig_t2 -- readable versions for err msgs x' = pfpReadable x orig_t1' = pfpReadable orig_t1 orig_t2' = pfpReadable orig_t2 -- return value mismatch err_res r1 r2 = err (getPosition x, EFuncMismatchResult x' orig_t1' orig_t2' (pfpReadable r1) (pfpReadable r2)) -- mismatch in the number of args err_wrong_arg_num n1 n2 = err (getPosition x, EFuncMismatchNumArgs x' orig_t1' orig_t2' n1 n2 Nothing) -- mismatch in num of args, but we know where the first -- type mismatch occurred, so maybe the arg is missing there? err_wrong_arg_num_maybe_n n1 n2 startnum = err (getPosition x, EFuncMismatchNumArgs x' orig_t1' orig_t2' n1 n2 (Just startnum)) -- mismatch in the type of argument n err_arg_n num a1 a2 = err (getPosition x, EFuncMismatchArgN x' orig_t1' orig_t2' num (pfpReadable a1) (pfpReadable a2)) -- not expecting args err_no_args_expected = err (getPosition x, EFuncMismatchNoArgsExpected x' orig_t1' orig_t2') -- expecting args, but given none err_args_expected n = err (getPosition x, EFuncMismatchArgsExpected x' orig_t1' orig_t2' n) -- This allows more unification that would actually be allowed -- because it does not take into account substitutions from previous -- unifications. Therefore a->a->a would match Bool->Int->Int. -- This is ok, because it will be reported with the default error. canUnify t1 t2 = case (mgu bound_vars t1 t2) of Nothing -> do -- call normT because unify does t1' <- normT t1 t2' <- normT t2 case (mgu bound_vars t1' t2') of Nothing -> return False Just _ -> return True Just _ -> return True -- find the number of arguments expected by a type findNumArgs :: Type -> Integer findNumArgs t = genericLength $ fst $ getArrows t -- Try to find the specific mismatch, else report the default -- mismatch error on the entire original type. -- The 'n' is the number of args which matched so far. findMismatch n (TAp (TAp (TCon arr1) a1) r1) (TAp (TAp (TCon arr2) a2) r2) | isTConArrow arr1 && isTConArrow arr2 = do b <- canUnify a1 a2 if (b) then findMismatch (n+1) r1 r2 else let num_args1 = n + 1 + findNumArgs r1 num_args2 = n + 1 + findNumArgs r2 in if (num_args1 == num_args2) then err_arg_n (n+1) a1 a2 else err_wrong_arg_num_maybe_n num_args1 num_args2 (n+1) findMismatch n (TAp (TAp (TCon arr1) a1) r1) t1 | isTConArrow arr1 = if (n == 0) then err_args_expected (1 + findNumArgs r1) else -- see if the return value matches? err_wrong_arg_num (n + 1 + findNumArgs r1) n findMismatch n t1 (TAp (TAp (TCon arr2) a2) r2) | isTConArrow arr2 = if (n == 0) then err_no_args_expected else err_wrong_arg_num n (n + 1 + findNumArgs r2) findMismatch n t1 t2 = if (n == 0) then def_err else do b <- canUnify t1 t2 if (b) then def_err -- couldn't find the mismatch else err_res t1 t2 in findMismatch 0 orig_t1 orig_t2 defaultUnifyError :: (HasPosition a, PPrint a, PVPrint a) => a -> Type -> Type -> TI d defaultUnifyError x t1 t2 = err (getPosition x, EUnify (pfpReadable x) (pfpReadable t1) (pfpReadable t2)) ----- -- unify e td (a `fn` rt) unifyFnFrom :: (HasPosition a, HasPosition b, PPrint b, PVPrint b) => a -> b -> Type -> Type -> TI (Type, [VPred]) unifyFnFrom x e (TAp (TAp arr a) r) rt | arr == tArrow = do ps <- unify e r rt return (a, ps) unifyFnFrom x e t rt = do {- s <- getSubst case apSub s t of (TAp (TAp arr a) r) | arr == tArrow -> do unify e r rt return a _ -> do -} v <- newTVar "unifyFnFrom" KStar x ps <- unify e t (v `fn` rt) return (v, ps) -- unify e td (at `fn` r) unifyFnTo :: (HasPosition a, HasPosition b, PPrint b, PVPrint b) => a -> b -> Type -> Type -> TI (Type, [VPred]) unifyFnTo x e (TAp (TAp arr a) r) at | arr == tArrow = do ps <- unify e a at return (r, ps) unifyFnTo x e t at = do {- s <- getSubst case apSub s t of (TAp (TAp arr a) r) | arr == tArrow -> do unify e a at return r _ -> do -} v <- newTVar "unifyFnTo" KStar x ps <- unify e t (at `fn` v) return (v, ps) -- because we merely break apart the type if it has function structure -- and create new type variables only if it doesn't -- we never do anything that might generate numeric equalities -- unify e td (a `fn` r) unifyFnFromTo :: (HasPosition a, HasPosition b, PPrint b, PVPrint b) => a -> b -> Type -> TI (Type, Type) unifyFnFromTo x e (TAp (TAp arr a) r) | arr == tArrow = do return (a, r) unifyFnFromTo x e t = do {- s <- getSubst case apSub s t of (TAp (TAp arr a) r) | arr == tArrow -> do return (a, r) _ -> do -} v <- newTVar "unifyFnFromTo" KStar x r <- newTVar "unifyFnFromTo" KStar x unifyNoEq "unifyFnFromTo" e t (v `fn` r) return (v, r) ----- -- clean up synonyms and TCons when VPreds are made -- they should not be re-introduced later (by predicate reduction)o mkVPred :: Position -> PredWithPositions -> TI [VPred] mkVPred pos p = do v <- newDict expTConPred (expandSynVPred $ VPred v (addPredPositions p [pos])) mkVPredNoNewPos :: PredWithPositions -> TI [VPred] mkVPredNoNewPos p = do v <- newDict expTConPred (expandSynVPred $ VPred v p) -- entry point when we don't need synonyms reduced -- mainly deriving and other places where we check reducibility mkVPredFromPred :: [Position] -> Pred -> TI VPred mkVPredFromPred poss p = do v <- newDict return (VPred v $ mkPredWithPositions poss p) toPredWithPositions :: VPred -> PredWithPositions toPredWithPositions (VPred _ p) = p toPred :: VPred -> Pred toPred p = removePredPositions (toPredWithPositions p) vpIsPreClass :: VPred -> Bool vpIsPreClass (VPred _ (PredWithPositions (IsIn cl _) _)) = isPreClass cl -- Close a set of variables with respect to predicates and their functional -- dependencies. -- In otherwords: Extend a set of variables to includes all the variables -- which depend on them, as indicated in a list of predicates. closeFD :: [VPred] -> [TyVar] -> [TyVar] closeFD ps vs = let ps' = map toPred ps in closeFD_pred ps' vs closeFD_pred :: [Pred] -> [TyVar] -> [TyVar] closeFD_pred ps vs = let -- extend given one dependency step1 ts bs vars_in_set = let dependee_exprs = (boolCompress (map not bs) ts) dependee_vars = tv dependee_exprs dependent_exprs = (boolCompress bs ts) dependent_vars = tv dependent_exprs in -- This intentionally includes situations where the dependee -- set is null if all (`elem` vars_in_set) dependee_vars then vars_in_set `union` dependent_vars else vars_in_set -- extend for all dependencies for a given predicate step p vars_in_set = let (IsIn c ts) = p in foldr (step1 ts) vars_in_set (funDeps c) vs' = foldr step vs ps in -- recurse until no new vars are found if (length vs == length vs') then vs else closeFD_pred ps vs' ------- -- Note that "t" can be a tuple of types, or list of types, or a predicate, -- because class Types just means that "t" *contains* types. niceTypes :: (Types t) => t -> t niceTypes given_type = let -- Variables in the given "t" type_vars :: [TyVar] type_vars = tv given_type type_var_names = map (getIdString . getTyVarId) type_vars -- Make an inexaustible list of nice names from_a_to_z prefix = [prefix ++ [letter] | letter <- ['a'..'z']] inexhaustible_var_names = (map (:[]) ['a'..'z'] ++ concatMap from_a_to_z inexhaustible_var_names) -- Make the names end with an identifiable suffix new_inexhaustible_var_names = -- and rule out any existing names filter (`notElem` type_var_names) $ map (\ s -> s ++ sAcute) inexhaustible_var_names -- Function to substitute in the new names subst_vars :: [TyVar] -> [String] -> [(TyVar, Type)] subst_vars (orig_var:rest_orig_vars) new_names@(new_name:rest_new_names) | isNewTVar orig_var = let new_id = -- preserve the "isNewTVar" property setBadId $ mkId (getPosition orig_var) (mkFString new_name) new_var = cTVarKind new_id (kind orig_var) in (orig_var, new_var) : subst_vars rest_orig_vars rest_new_names | otherwise = subst_vars rest_orig_vars new_names subst_vars [] _ = [] subst_vars _ [] = internalError ("TCMisc.niceTypes: " ++ "inexhaustible name supply exhausted") -- Create a substitution pairing the existing vars with the new var_subst_pairs = subst_vars type_vars new_inexhaustible_var_names substitution = mkSubst var_subst_pairs in apSub substitution given_type ------- -- The following code is for defaulting types when an explicit type -- declaration is reached but for which type inference has inferred -- more contexts than appear in the explicit type. Any contexts which -- have variables that appear in the base type result in "context too -- weak" errors. For multi-parameter type classes, if some variables -- are not in the base type, we may want to default them, which could -- cause the context to be resolved. -- In the following code we define the classes that are defaultable -- and how to compute potential default assignments from an -- unsatisfied predicate. Defaulting can fill in, at most, one -- "hole" (i.e. potentially ambiguous type variable) in a predicate. -- Some classes (e.g. Literal) have multiple defaults worth trying -- while others (e.g. BitExtend) need to compute the default from -- the other arguments of the predicate. -- Ideally, Pred.Class would have a field "getDefaults" that would replace -- getStarDefaults / getNumDefaults, but we'd need syntax for specifying -- the defaults for of a class (steal / extend the Haskell' proposal?) -- If more than one class proposes defaults for a particular -- ambiguous type variable, we currently intersect the proposed defaults -- (which handles the PrimIndex/Literal/RealLiteral possible overlap with -- no wasted work). In some cases (particularly if we made defaults more -- general) it might be better to union the proposed defaults. -- Classes with *-kind types which can be defaulted getStarDefaults :: S.Set TyVar -> VPred -> [(TyVar, [Type])] getStarDefaults fvs (VPred i (PredWithPositions (IsIn (Class {name=(CTypeclass cid)}) ts) _)) = case ts of [TVar v, _] | cid == idPrimIndex, not (S.member v fvs) -> [(v, [tInteger, tNat noPosition])] [TVar v] | cid == idLiteral, not (S.member v fvs) -> [(v, [tInteger, tNat noPosition, tReal])] [TVar v] | cid == idRealLiteral, not (S.member v fvs) -> [(v, [tReal])] [TVar v, n] | cid == idSizedLiteral, not (S.member v fvs) -> [(v, [TAp tBit n, TAp tUInt n, TAp tInt n])] [TVar v] | cid == idStringLiteral, not (S.member v fvs) -> [(v, [tString, tChar])] _ -> [] -- Classes with #-kind types which can be defaulted getNumDefaults :: S.Set TyVar -> VPred -> [(TyVar, [Type])] getNumDefaults fvs (VPred i (PredWithPositions (IsIn (Class {name=(CTypeclass cid)}) ts) _)) = case ts of [TVar v, t, _] | cid == idBitExtend, not (S.member v fvs), all (flip S.member $ fvs) (tv t) -> [(v, [t])] [t, TVar v, _] | cid == idBitExtend, not (S.member v fvs), all (flip S.member $ fvs) (tv t) -> [(v, [t])] [TVar v, t, _] | cid == idAdd, not (S.member v fvs), all (flip S.member $ fvs) (tv t) -> [(v, [cTNum 0 noPosition])] [t, TVar v, _] | cid == idAdd, not (S.member v fvs), all (flip S.member $ fvs) (tv t) -> [(v, [cTNum 0 noPosition])] _ -> [] getForceDefaults :: S.Set TyVar -> VPred -> [(TyVar, Type)] getForceDefaults fvs (VPred i (PredWithPositions (IsIn (Class {name=(CTypeclass cid)}) ts) _)) = case ts of [TVar v] | cid == idStringLiteral, not (S.member v fvs) -> [(v, tString)] _ -> [] -- Takes -- fixedVars = list of variables from the base type unioned with a -- list of variables from the context (bound variables, assumptions) -- givenPreds = explicit predicates provided by the user -- unsatisfiedPreds = unsatisfied predicates on the base type -- -- Then, the function identifies ambiguous variables in the predicates -- and tries to default them. -- -- It returns: -- any unsatisfied predicates, -- any bindings resulting from satisfying predicates, and -- any remaining ambiguous type variables (which were not defaultable or -- defaulting didn't succeed). -- defaultClasses :: [TyVar] -> [EPred] -> [VPred] -> TI ([VPred], [CDefl], [TyVar]) defaultClasses fixedVars givenPreds unsatisfiedPreds = let -- all variables which are not ambiguous fixedVars_closed = closeFD unsatisfiedPreds fixedVars fixedVarsSet :: S.Set TyVar fixedVarsSet = S.fromList fixedVars_closed -- whether a substitution substitutes for a fixed variable -- (we use "fixedVars_closed" because we do not want to limit the -- fixed variables at all; we'd rather report an ambiguity error) subsFixedVar s = any (`S.member` fixedVarsSet) (getSubstDomain s) -- identify the ambiguous variables -- (we leave it to "handleAmbiguousContext" to filter out any ambig -- vars that are determined by other ambig vars) ambVarsSet :: S.Set TyVar ambVarsSet = S.fromList (concatMap tv unsatisfiedPreds) `S.difference` fixedVarsSet isAmbiguousVar v = S.member v ambVarsSet preds_with_vars :: [(VPred, [TyVar])] preds_with_vars = [(p, filter isAmbiguousVar (tv p)) | p <- unsatisfiedPreds ] -- produce a list of -- pairs of ambiguous vars and the preds they appear in vars_with_preds :: [(TyVar, [VPred])] vars_with_preds = M.toList . (M.fromListWith (++)) $ [(v,[p]) | (p, vs) <- preds_with_vars, v <- vs] preds_to_default = map fst preds_with_vars num_defaults :: [(TyVar, [Type])] num_defaults = concatMap (getNumDefaults fixedVarsSet) preds_to_default star_defaults :: [(TyVar, [Type])] star_defaults = concatMap (getStarDefaults fixedVarsSet) preds_to_default defaultsMap :: M.Map TyVar [Type] defaultsMap = M.fromListWith (intersect) $ num_defaults ++ star_defaults -- Given a type variable, a list of predicates in which it -- appears, and a type to default to, substitute the default -- for the variable in the predicates and determine if "sat" -- succeeds for all predicates. If so, return that substitution. -- If a substitution was found by a prior call, just pass its -- value through. tryDefault :: TyVar -> [VPred] -> (Maybe Subst) -> Type -> TI (Maybe Subst) tryDefault i ps Nothing t = do let s = mkSubst [(i,t)] ps' = apSub s ps answer <- satMany (Just fixedVars) givenPreds [] [] s ps' return $ case answer of -- we reject this default if it does not work for some pred -- or if it results in a substitution of a bound variable ([], _, s') | not $ subsFixedVar s' -> Just s' _ -> Nothing tryDefault i ps s@(Just _) t = return s tryDefaults :: Subst -> (TyVar, [VPred]) -> TI Subst tryDefaults subst (i,ps) = do let typesToTry = M.findWithDefault [] i defaultsMap r <- foldM (tryDefault i ps) Nothing typesToTry return $ case r of Nothing -> subst -- only merge agreements so we are (mostly) -- order-independent Just s -> mergeAgreements s subst -- take a new subst and the remaining unsatisfied preds, and simplify makeResult amb_set s ps = do -- see how many total preds are satisfied now -- this is different because we're trying to satisfy preds -- whether or not they contain ambiguous vars (remaining_ps, new_bindings) <- satisfyFV fixedVars givenPreds (apSub s ps) -- find the remaining ambiguous variables -- (this used to intersect the tyvars of the remaining preds with -- the original set of ambig vars, but that doesn't work after -- forcing, only after defaulting, so we do the real calculation) let new_fixedVarsSet = S.fromList (closeFD remaining_ps fixedVars) remaining_amb_set = S.fromList (concatMap tv remaining_ps) `S.difference` new_fixedVarsSet return (remaining_ps, new_bindings, remaining_amb_set) in if (S.null ambVarsSet) then -- no defaulting to do return (unsatisfiedPreds, [], []) else do let s0 = nullSubst s1 <- foldM tryDefaults s0 vars_with_preds let defaulted_vars = getSubstDomain s1 -- extend the substitution extSubst "defaultClasses" s1 -- numeric defaulting is now an unknown-size error let mkNumError v | v `elem` defaulted_vars = [(getPosition v, EUnknownSize)] | otherwise = [] msgs = nub $ concatMap (mkNumError . fst) num_defaults when (not $ null msgs) $ errs "defaultClasses unknown size" msgs -- simplify, given what we know (remaining_preds, new_bindings, remaining_amb_set) <- makeResult ambVarsSet s1 unsatisfiedPreds -- see if we need to force any preds let typesToForce = concatMap (getForceDefaults fixedVarsSet) remaining_preds if (null typesToForce) then return (remaining_preds, new_bindings, S.toList remaining_amb_set) else do -- otherwise, force these variables and simplify again (res_ps, res_bs, res_aset) <- makeResult remaining_amb_set (mkSubst typesToForce) remaining_preds -- XXX issue a warning that the types have been forced? return (res_ps, res_bs, S.toList res_aset) ------- -- Given the fixed variables from the context (that is, any vars in -- the assumptions and any bound vars) and a qualified type, determine -- if any of the preds in the qualified type are unsatisfiabl because -- they contain variables not fixed by the caller. checkForAmbiguousPreds :: Id -> [TyVar] -> Qual Type -> TI () checkForAmbiguousPreds i fvs1 qt = do -- in order to catch ambiguous variables arising from uses of TLog etc, -- expand such TCons into additional predicates (qs :=> t) <- expandNumericTCons qt let -- the explicit predicates ps = map removePredPositions qs -- fixed vars from the base type fvs2 = tv t -- all fixed vars fvs = fvs1 `union` fvs2 -- close the fixed vars over fundeps cfvs = closeFD_pred ps fvs -- ambiguous variables in the predicates amb_vars = tv ps \\ cfvs hasAmbigVar p = any (`elem` amb_vars) (tv p) -- ambiguous predicates amb_preds = filter hasAmbigVar ps -- pprint pfp :: (PPrint a, PVPrint a) => a -> Doc pfp = pfPrint PDReadable 0 -- rename generated typevars with "a__", "b__", etc -- (names are only generated by TCon expansion) (amb_preds', amb_vars', t') = niceTypes (amb_preds, map TVar amb_vars, t) if (null amb_vars) then return () else err (getPosition i, EAmbiguousExplCtx (map pfp amb_vars') (map pfp amb_preds') (pfp t')) expandNumericTCons :: Qual Type -> TI (Qual Type) expandNumericTCons (orig_qs :=> orig_t) = let mkResult cls_id ts v = do symt <- getSymTab let cls = mustFindClass symt (CTypeclass cls_id) p = PredWithPositions (IsIn cls ts) [] return ([p], v) expQual :: PredWithPositions -> TI ([PredWithPositions], PredWithPositions) expQual (PredWithPositions (IsIn c ts) poss) = do (qs, ts') <- mapM exp ts >>= return . apFst concat . unzip return (qs, PredWithPositions (IsIn c ts') poss) -- all TCon could be expanded as NumEq#(var,TC) but we go ahead and -- expand to the associate typeclass (is this better for err msgs?) exp :: Type -> TI ([PredWithPositions], Type) exp (TAp tc t) | tc == tLog = do v <- newTVar "expandNumericTCons" KNum tc mkResult idLog [t, v] v | tc == tExp = do v <- newTVar "expandNumericTCons" KNum tc -- There's no class for this, so use NumEq mkResult idNumEq [v, TAp tc t] v | tc == tSizeOf = do v <- newTVar "expandNumericTCons" KNum tc mkResult idBits [t, v] v exp (TAp (TAp tc t1) t2) | tc == tAdd = do v <- newTVar "expandNumericTCons" KNum tc mkResult idAdd [t1, t2, v] v | tc == tSub = do v <- newTVar "expandNumericTCons" KNum tc mkResult idAdd [t1, v, t2] v | tc == tMul = do v <- newTVar "expandNumericTCons" KNum tc mkResult idMul [t1, t2, v] v | tc == tDiv = do v <- newTVar "expandNumericTCons" KNum tc mkResult idDiv [t1, t2, v] v | tc == tMax = do v <- newTVar "expandNumericTCons" KNum tc mkResult idMax [t1, t2, v] v | tc == tMin = do v <- newTVar "expandNumericTCons" KNum tc mkResult idMin [t1, t2, v] v exp (TAp t1 t2) = do (ps1, t1') <- exp t1 (ps2, t2') <- exp t2 return (ps1 ++ ps2, TAp t1' t2') exp t = return ([], t) in do (new_qs1, orig_qs') <- mapM expQual orig_qs >>= return . apFst concat . unzip (new_qs2, orig_t') <- exp orig_t return ((new_qs1 ++ new_qs2 ++ orig_qs') :=> orig_t') ------- -- Propagation of functional dependencies was more complex -- before we required fundeps to be full. Now that we have, -- propagateFunDeps just uses satisfy (for full fundeps, -- propagation and matching are the same thing). -- propagateFunDeps returns the supplied predicates updated with -- any information learned by matching instances. It does not -- drop any matched predicates because it doesn't bind dictionaries. -- propagateFunDeps also returns the (possibly smaller) list of -- unsatisfied predicates for use in fail-fast context reduction -- (see updateContexts) propagateFunDeps :: [VPred] -> TI ([VPred], [VPred]) propagateFunDeps ps0 = do s <- getSubst eps <- getExplPreds let ps = apSub s ps0 satTraceM("propagateFunDeps satisfy: " ++ ppReadable ps) -- SAT solving of numeric provisos isn't needed for propagating fundeps, -- so turn it off, since it appears to be expensive here flags <- getFlags setFlags (flags { useProvisoSAT = False }) (ps_unsat, _) <- satisfy eps ps -- restore the flags setFlags flags s' <- getSubst return (apSub s' ps, ps_unsat) ------- -- like "reducePred", but we want to differentiate between those which -- don't reduce now (not enough type info yet) and those which could -- never reduce (which we'll want to report an error about now, not later) -- isReduciblePred :: VPred -> TI Bool isReduciblePred (VPred i pp@(PredWithPositions p@(IsIn c ts) pos)) | -- XXX for now, we don't consider Add, Max, Min, Log, Mul, Div, NumEq -- XXX (the "genInsts" of these classes doesn't handle "maybe reducible") (isPreClass c) = return True isReduciblePred (VPred i pp@(PredWithPositions p@(IsIn c ts) pos)) = do ts' <- mapM normT ts let p' = IsIn c ts' pp' = PredWithPositions p' pos v' = VPred i pp' f [] = getExplPreds >>= g f (i:is) = do isReducible <- byInstIsReducible v' i -- if we discover that it could match or definitely -- does not match, then stop; otherwise, try the -- remaining instances case (isReducible) of Fails -> return False Matches -> return True _ -> f is g [] = return False g (ep:eps) = do isReducible <- byExplPredIsReducible v' ep case (isReducible) of Fails -> return False Matches -> return True _ -> g eps bvs <- getBoundTVs let is' = genInsts c bvs Nothing p' r <- f is' return r data MatchResult = NoConclusion | Fails | Matches deriving (Eq) byInstIsReducible :: VPred -> Inst -> TI MatchResult byInstIsReducible (VPred i p) ii = do (mv, Inst e _ (ps :=> h)) <- newInst ii (getPredPositions p) bound_tyvars <- getBoundTVs return $ matchTopIsReducible bound_tyvars h (removePredPositions p) -- This is like "matchTop" except that we need to try matching first -- and if it fails, then we try unifying. Also, when we try matching, -- we need to differentiate between failure to match the non-fundep types -- (which means we still have a chance of matching somewhere else) and -- matching the non-fundep types but failing to match the dependent types -- (which is an immediate error, because the fundeps should be unique). -- Returns: -- * Nothing if the predicate can be proven unsatisfiable (because the -- fundeps don't match the unique instance) -- * Just False if the predicate does not match any existing instances -- * Just True if the predicate has a chance of matching an existing instance matchTopIsReducible :: [TyVar] -> Pred -> Pred -> MatchResult matchTopIsReducible bound_tyvars p1@(IsIn c1 ts1) p2@(IsIn c2 ts2) = if c1 /= c2 then NoConclusion else let try_match :: [Bool] -> MatchResult try_match bs = let nbs = map not bs v1 = (boolCompress nbs ts1) v2 = (boolCompress nbs ts2) -- whether the non-fundeps match mv = matchList v1 v2 -- whether the non-fundeps unify uv = mgu bound_tyvars v1 v2 -- check if the fundeps unify, given a subst for non-fundeps check_fds s = case (mgu bound_tyvars (apSub s (boolCompress bs ts1)) (apSub s (boolCompress bs ts2))) of Nothing -> False Just _ -> True in case (mv) of Nothing -> -- doesn't match, so try unify case (uv) of Nothing -> NoConclusion Just (s,num_eqs) -> if (check_fds s && null num_eqs) then Matches else NoConclusion Just s -> -- it matches, so we have a conclusive answer if (check_fds s) then Matches else -- we'd like to return Fails, but to support -- overlapping instances which disagree on the -- fundeps, we have to accept that there could -- be an overlapping instance where it matches --Fails NoConclusion in pickFirst (map try_match (funDeps c1)) pickFirst :: [MatchResult] -> MatchResult pickFirst mbs = if (any (== Matches) mbs) then Matches else if (any (== Fails) mbs) then Fails else NoConclusion byExplPredIsReducible :: VPred -> EPred -> TI MatchResult byExplPredIsReducible (VPred _ p) (EPred _ ep) = do bound_tyvars <- getBoundTVs return $ matchExplPred bound_tyvars (removePredPositions p) ep matchExplPred :: [TyVar] -> Pred -> Pred -> MatchResult matchExplPred bound_tyvars p1@(IsIn c1 ts1) p2@(IsIn c2 ts2) = if c1 /= c2 then NoConclusion else case (matchList ts1 ts2) of Nothing -> NoConclusion Just s -> Matches -------