git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/TypeSearch.hs
540 lines 23 kB history raw
1{-# LANGUAGE ScopedTypeVariables #-}
3module Idris.TypeSearch (
4 searchByType, searchPred, defaultScoreFunction
5) where
7import Control.Applicative (Applicative (..), (<$>), (<*>), (<|>))
8import Control.Arrow (first, second, (&&&), (***))
9import Control.Monad (when, guard)
11import Data.List (find, partition, (\\))
12import Data.Map (Map)
13import qualified Data.Map as M
14import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
15import Data.Monoid (Monoid (mempty, mappend))
16import Data.Ord (comparing)
17import qualified Data.PriorityQueue.FingerTree as Q
18import Data.Set (Set)
19import qualified Data.Set as S
20import qualified Data.Text as T (pack, isPrefixOf)
21import Data.Traversable (traverse)
23import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)
24import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,
25 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
26 implicitAllowed, OutputMode(..), PTerm, toplevel)
27import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
28import Idris.Core.TT hiding (score)
29import Idris.Core.Unify (match_unify)
30import Idris.Delaborate (delabTy)
31import Idris.Docstrings (noDocs, overview)
32import Idris.Elab.Type (elabType)
33import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)
34import Idris.IBC
36import Prelude hiding (pred)
38import Util.Pretty (text, char, vsep, (<>), Doc, annotate)
40searchByType :: [String] -> PTerm -> Idris ()
41searchByType pkgs pterm = do
42 i <- getIState -- save original
43 when (not (null pkgs)) $
44 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
46 mapM_ loadPkgIndex pkgs
47 pterm' <- addUsingConstraints syn emptyFC pterm
48 pterm'' <- implicit toplevel syn name pterm'
49 let pterm''' = addImpl [] i pterm''
50 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
51 let names = searchUsing searchPred i ty
52 let names' = take numLimit names
53 let docs =
54 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
55 displayScore theScore <> char ' ' <> prettyDocumentedIst i docInfo
56 | (n, theScore) <- names']
57 if (not (null docs))
58 then case idris_outputmode i of
59 RawOutput _ -> do mapM_ iRenderOutput docs
60 iPrintResult ""
61 IdeMode _ _ -> iRenderResult (vsep docs)
62 else iRenderError $ text "No results found"
63 putIState i -- don't actually make any changes
64 where
65 numLimit = 50
66 syn = defaultSyntax { implicitAllowed = True } -- syntax
67 name = sMN 0 "searchType" -- name
69-- | Conduct a type-directed search using a given match predicate
70searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
71 -> IState -> Type -> [(Name, a)]
72searchUsing pred istate ty = pred istate nty . concat . M.elems $
73 M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
74 where
75 nty = normaliseC ctxt [] ty
76 ctxt = tt_ctxt istate
77 f k x = do
78 guard $ not (special k)
79 type2 <- typeFromDef x
80 return $ normaliseC ctxt [] type2
81 special :: Name -> Bool
82 special (NS n _) = special n
83 special (SN _) = True
84 special (UN n) = T.pack "default#" `T.isPrefixOf` n
85 || n `elem` map T.pack ["believe_me", "really_believe_me"]
86 special _ = False
88-- | Our default search predicate.
89searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
90searchPred istate ty1 = matcher where
91 maxScore = 100
92 matcher = matchTypesBulk istate maxScore ty1
95typeFromDef :: (Def, b, c, d) -> Maybe Type
96typeFromDef (def, _, _, _) = get def where
97 get :: Def -> Maybe Type
98 get (Function ty _) = Just ty
99 get (TyDecl _ ty) = Just ty
100 -- get (Operator ty _ _) = Just ty
101 get (CaseOp _ ty _ _ _ _) = Just ty
102 get _ = Nothing
104-- Replace all occurences of `Lazy' s t` with `t` in a type
105unLazy :: Type -> Type
106unLazy typ = case typ of
107 App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty
108 Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)
109 App s t1 t2 -> App s (unLazy t1) (unLazy t2)
110 Proj ty i -> Proj (unLazy ty) i
111 _ -> typ
113-- | reverse the edges for a directed acyclic graph
114reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
115reverseDag xs = map f xs where
116 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)
118-- run vToP first!
119-- | Compute a directed acyclic graph corresponding to the
120-- arguments of a function.
121-- returns [(the name and type of the bound variable
122-- the names in the type of the bound variable)]
123computeDagP :: Ord n
124 => (TT n -> Bool) -- ^ filter to remove some arguments
125 -> TT n
126 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
127computeDagP removePred t = (reverse (map f arguments), reverse theRemovedArgs , retTy) where
128 f (n, ty) = ((n, ty), M.keysSet (usedVars ty))
130 (arguments, theRemovedArgs, retTy) = go [] [] t
132 -- NOTE : args are in reverse order
133 go args removedArgs (Bind n (Pi _ ty _) sc) = let arg = (n, ty) in
134 if removePred ty
135 then go args (arg : removedArgs) sc
136 else go (arg : args) removedArgs sc
137 go args removedArgs sc = (args, removedArgs, sc)
139-- | Collect the names and types of all the free variables
140-- The Boolean indicates those variables which are determined due to injectivity
141-- I have not given nearly enough thought to know whether this is correct
142usedVars :: Ord n => TT n -> Map n (TT n, Bool)
143usedVars = f True where
144 f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t
145 f b (Bind n binder t2) = (M.delete n (f b t2) `M.union`) $ case binder of
146 Let t v -> f b t `M.union` f b v
147 Guess t v -> f b t `M.union` f b v
148 bind -> f b (binderTy bind)
149 f b (App _ t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
150 f b (Proj t _) = f b t
151 f _ (V _) = error "unexpected! run vToP first"
152 f _ _ = M.empty
154-- | Remove a node from a directed acyclic graph
155deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
156deleteFromDag name [] = []
157deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
158 then id
159 else (((name2, ty) , (ix, S.delete name set)) :) ) (deleteFromDag name xs)
161deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
162deleteFromArgList n = filter ((/= n) . fst)
164-- | Asymmetric modifications to keep track of
165data AsymMods = Mods
166 { argApp :: !Int
167 , typeClassApp :: !Int
168 , typeClassIntro :: !Int
169 } deriving (Eq, Show)
172-- | Homogenous tuples
173data Sided a = Sided
174 { left :: !a
175 , right :: !a
176 } deriving (Eq, Show)
178sided :: (a -> a -> b) -> Sided a -> b
179sided f (Sided l r) = f l r
181-- | Could be a functor instance, but let's avoid name overloading
182both :: (a -> b) -> Sided a -> Sided b
183both f (Sided l r) = Sided (f l) (f r)
185-- | Keeps a record of the modifications made to match one type
186-- signature with another
187data Score = Score
188 { transposition :: !Int -- ^ transposition of arguments
189 , equalityFlips :: !Int -- ^ application of symmetry of equality
190 , asymMods :: !(Sided AsymMods) -- ^ "directional" modifications
191 } deriving (Eq, Show)
193displayScore :: Score -> Doc OutputAnnotation
194displayScore score = case both noMods (asymMods score) of
195 Sided True True -> annotated EQ "=" -- types are isomorphic
196 Sided True False -> annotated LT "<" -- found type is more general than searched type
197 Sided False True -> annotated GT ">" -- searched type is more general than found type
198 Sided False False -> text "_"
199 where
200 annotated ordr = annotate (AnnSearchResult ordr) . text
201 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
203-- | This allows the search to stop expanding on a certain state if its
204-- score is already too high. Returns 'True' if the algorithm should keep
205-- exploring from this state, and 'False' otherwise.
206scoreCriterion :: Score -> Bool
207scoreCriterion (Score _ _ amods) = not
208 ( sided (&&) (both ((> 0) . argApp) amods)
209 || sided (+) (both argApp amods) > 4
210 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
211 )
213-- | Convert a 'Score' to an 'Int' to provide an order for search results.
214-- Lower scores are better.
215defaultScoreFunction :: Score -> Int
216defaultScoreFunction (Score trans eqFlip amods) =
217 trans + eqFlip + linearPenalty + upAndDowncastPenalty
218 where
219 -- prefer finding a more general type to a less general type
220 linearPenalty = (\(Sided l r) -> 3 * l + r)
221 (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)
222 -- it's very bad to have *both* upcasting and downcasting
223 upAndDowncastPenalty = 100 *
224 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
226instance Ord Score where
227 compare = comparing defaultScoreFunction
230instance Monoid a => Monoid (Sided a) where
231 mempty = Sided mempty mempty
232 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)
234instance Monoid AsymMods where
235 mempty = Mods 0 0 0
236 (Mods a b c) `mappend` (Mods a' b' c') = Mods (a + a') (b + b') (c + c')
238instance Monoid Score where
239 mempty = Score 0 0 mempty
240 (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')
242-- | A directed acyclic graph representing the arguments to a function
243-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
244type ArgsDAG = [((Name, Type), (Int, Set Name))]
246-- | A list of typeclass constraints
247type Classes = [(Name, Type)]
249-- | The state corresponding to an attempted match of two types.
250data State = State
251 { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
252 , argsAndClasses :: !(Sided (ArgsDAG, Classes))
253 -- ^ arguments and typeclass constraints for each type which have yet to be resolved
254 , score :: !Score -- ^ the score so far
255 , usedNames :: ![Name] -- ^ all names that have been used
256 } deriving Show
258modifyTypes :: (Type -> Type) -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
259modifyTypes f = modifyDag *** modifyList
260 where
261 modifyDag = map (first (second f))
262 modifyList = map (second f)
264findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
265findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst)
267findName :: Name -> (ArgsDAG, Classes) -> Maybe (Type, Maybe Int)
268findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n classes <*> Nothing)
270deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)
271deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes)
273tcToMaybe :: TC a -> Maybe a
274tcToMaybe (OK x) = Just x
275tcToMaybe (Error _) = Nothing
277inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
278inArgTys = map . first . second
281typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
282typeclassUnify classInfo ctxt ty tyTry = do
283 res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []
284 guard $ null (theHoles \\ map fst res)
285 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
286 return argTys'
287 where
288 tyTry' = vToP tyTry
289 theHoles = map fst nonTcArgs
290 retTy = getRetTy tyTry'
291 (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
293isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool
294isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
295 (clss, args) = unApply ty
296 getClassName (P (TCon _ _) className _) = [className]
297 getClassName _ = []
300-- | Compute the power set
301subsets :: [a] -> [[a]]
302subsets [] = [[]]
303subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss
306-- not recursive (i.e., doesn't flip iterated identities) at the moment
307-- recalls the number of flips that have been made
308flipEqualities :: Type -> [(Int, Type)]
309flipEqualities t = case t of
310 eq1@(App _ (App _ (App _ (App _ eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->
311 [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]
312 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))
313 <$> traverse flipEqualities binder <*> flipEqualities sc
314 App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))
315 <$> flipEqualities f <*> flipEqualities x
316 t' -> [(0, t')]
317 where app = App Complete
319--DONT run vToP first!
320-- | Try to match two types together in a unification-like procedure.
321-- Returns a list of types and their minimum scores, sorted in order
322-- of increasing score.
323matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
324matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
325 getStartQueues :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
326 getStartQueues nty@(info, type2) = case mapMaybe startStates ty2s of
327 [] -> Nothing
328 xs -> Just (minimum (map fst xs), (info, Q.fromList xs))
329 where
330 ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
331 <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
332 flipEqualitiesDag dag = case dag of
333 [] -> [(0, [])]
334 ((n, ty), (pos, deps)) : xs ->
335 (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))
336 <$> flipEqualities ty <*> flipEqualitiesDag xs
337 startStates (numEqFlips, sndDag, sndRetTy) = do
338 state <- unifyQueue (State startingHoles
339 (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))
340 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
341 return (score state, state)
344 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
345 argNames2 = map fst dag2
346 usedns = map fst startingHoles
347 startingHoles = argNames1 ++ argNames2
349 startingTypes = [(retTy1, retTy2)]
352 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
353 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types
355 getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
356 getAllResults q = case Q.minViewWithKey q of
357 Nothing -> []
358 Just ((nextScore, (info, stateQ)), q') ->
359 if defaultScoreFunction nextScore <= maxScore
360 then case nextStepsQueue stateQ of
361 Nothing -> getAllResults q'
362 Just (Left stateQ') -> case Q.minViewWithKey stateQ' of
363 Nothing -> getAllResults q'
364 Just ((newQscore,_), _) -> getAllResults (Q.add newQscore (info, stateQ') q')
365 Just (Right theScore) -> (info, theScore) : getAllResults q'
366 else []
369 ctxt = tt_ctxt istate
370 classInfo = idris_classes istate
372 (dag1, typeClassArgs1, retTy1) = makeDag type1
373 argNames1 = map fst dag1
374 makeDag :: Type -> (ArgsDAG, Classes, Type)
375 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
376 computeDagP (isTypeClassArg classInfo) . vToP . unLazy
377 first3 f (a,b,c) = (f a, b, c)
379 -- update our state with the unification resolutions
380 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
381 resolveUnis [] state = Just (state, [])
382 resolveUnis ((name, term@(P Bound name2 _)) : xs)
383 state | isJust findArgs = do
384 ((ty1, ix1), (ty2, ix2)) <- findArgs
386 (state'', queue) <- resolveUnis xs state'
387 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
388 return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
389 where
390 unresolved = argsAndClasses state
391 inScore f stat = stat { score = f (score stat) }
392 findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|>
393 ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved))
394 matchnames = [name, name2]
395 deleteArgs = deleteName name . deleteName name2
396 state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state)
397 , argsAndClasses = both (modifyTypes (subst name term) . deleteArgs) unresolved}
399 resolveUnis ((name, term) : xs)
400 state@(State hs unresolved _ _) = case both (findName name) unresolved of
401 Sided Nothing Nothing -> Nothing
402 Sided (Just _) (Just _) -> error "Idris internal error: TypeSearch.resolveUnis"
403 oneOfEach -> first (addScore (both scoreFor oneOfEach)) <$> nextStep
404 where
405 scoreFor (Just _) = mempty { argApp = 1 }
406 scoreFor Nothing = mempty { argApp = otherApplied }
407 -- find variables which are determined uniquely by the type
408 -- due to injectivity
409 matchedVarMap = usedVars term
410 bothT f (x, y) = (f x, f y)
411 (injUsedVars, notInjUsedVars) = bothT M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst hs) $ M.map snd matchedVarMap
412 varsInTy = injUsedVars ++ notInjUsedVars
413 toDelete = name : varsInTy
414 deleteMany = foldr (.) id (map deleteName toDelete)
416 otherApplied = length notInjUsedVars
418 addScore additions theState = theState { score = let s = score theState in
419 s { asymMods = asymMods s `mappend` additions } }
420 state' = state { holes = filter (not . (`elem` toDelete) . fst) hs
421 , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }
422 nextStep = resolveUnis xs state'
425 -- | resolve a queue of unification constraints
426 unifyQueue :: State -> [(Type, Type)] -> Maybe State
427 unifyQueue state [] = return state
428 unifyQueue state ((ty1, ty2) : queue) = do
429 --trace ("go: \n" ++ show state) True `seq` return ()
430 res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]
431 (ty1, Nothing)
432 (ty2, Nothing) [] (map fst $ holes state) []
433 (state', queueAdditions) <- resolveUnis res state
434 guard $ scoreCriterion (score state')
435 unifyQueue state' (queue ++ queueAdditions)
437 possClassInstances :: [Name] -> Type -> [Type]
438 possClassInstances usedns ty = do
439 className <- getClassName clss
440 classDef <- lookupCtxt className classInfo
441 n <- class_instances classDef
442 def <- lookupCtxt n (definitions ctxt)
443 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
444 let ty' = vToP (uniqueBinders usedns nty)
445 return ty'
446 where
447 (clss, _) = unApply ty
448 getClassName (P (TCon _ _) className _) = [className]
449 getClassName _ = []
451 -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has
452 -- 'Left' if we haven't found a terminal state, 'Right' if we have
453 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
454 nextStepsQueue queue = do
455 ((nextScore, next), rest) <- Q.minViewWithKey queue
456 Just $ if isFinal next
457 then Right nextScore
458 else let additions = if scoreCriterion nextScore
459 then Q.fromList [ (score state, state) | state <- nextSteps next ]
460 else Q.empty in
461 Left (Q.union rest additions)
462 where
463 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
464 isFinal _ = False
466 -- | Find all possible matches starting from a given state.
467 -- We go in stages rather than concatenating all three results in hopes of narrowing
468 -- the search tree. Once we advance in a phase, there should be no going back.
469 nextSteps :: State -> [State]
471 -- Stage 3 - match typeclasses
472 nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =
473 if null results3 then results4 else results3
474 where
475 -- try to match a typeclass argument from the left with a typeclass argument from the right
476 results3 =
477 catMaybes [ unifyQueue (State []
478 (Sided ([], deleteFromArgList n1 c1)
479 ([], map (second subst2for1) (deleteFromArgList n2 c2)))
480 scoreAcc usedns) [(ty1, ty2)]
481 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
483 -- try to hunt match a typeclass constraint by replacing it with an instance
484 results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)
485 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
486 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
487 | sds <- allMods ]
488 where
489 allMods = parallel defMod mods
490 mods :: Sided [( Classes, AsymMods, [Name] )]
491 mods = both (instanceMods . snd) unresolved
492 defMod :: Sided (Classes, AsymMods, [Name])
493 defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved
494 parallel :: Sided a -> Sided [a] -> [Sided a]
495 parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs
496 instanceMods :: Classes -> [( Classes , AsymMods, [Name] )]
497 instanceMods classes = [ ( newClassArgs, mempty { typeClassApp = 1 }, newHoles )
498 | (_, ty) <- classes
499 , inst <- possClassInstances usedns ty
500 , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
501 , let newHoles = map fst newClassArgs ]
504 -- Stage 1 - match arguments
505 nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where
507 results = concatMap takeSomeClasses results1
509 -- we only try to match arguments whose names don't appear in the types
510 -- of any other arguments
511 canBeFirst :: ArgsDAG -> [(Name, Type)]
512 canBeFirst = map fst . filter (S.null . snd . snd)
514 -- try to match an argument from the left with an argument from the right
515 results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)
516 (Sided (deleteFromDag n1 dagL, c1)
517 (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))
518 scoreAcc usedns) [(ty1, ty2)]
519 | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR
520 , let subst2for1 = psubst n2 (P Bound n1 ty1)]
524 -- Stage 2 - simply introduce a subset of the typeclasses
525 -- we've finished, so take some classes
526 takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
527 map statesFromMods . prod $ both (classMods . snd) unresolved
528 where
529 swap (Sided l r) = Sided r l
530 statesFromMods :: Sided (Classes, AsymMods) -> State
531 statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides
532 mods = swap (both snd sides) in
533 State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
534 classMods :: Classes -> [(Classes, AsymMods)]
535 classMods cs = let lcs = length cs in
536 [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]
537 prod :: Sided [a] -> [Sided a]
538 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]
539 -- still have arguments to match, so just be the identity
540 takeSomeClasses s = [s]