@@ -7,20 +7,21 @@ import Control.Arrow (first, second, (&&&))
77import Control.Monad (forM_, guard)
88
99import Data.Function (on)
10−import Data.List (find, minimumBy, sortBy, (\\))
10+import Data.List (find, minimumBy, partition, sortBy, (\\))
1111import Data.Map (Map)
1212import qualified Data.Map as M
1313import Data.Maybe (catMaybes, fromMaybe, isJust)
1414import Data.Monoid (Monoid (mempty, mappend))
1515import Data.Set (Set)
1616import qualified Data.Set as S
17+import qualified Data.Text as T (pack, isPrefixOf)
1718
1819import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
1920import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
2021 IState (idris_classes, idris_docstrings, tt_ctxt),
2122 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
2223import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
23−import Idris.Core.TT
24+import Idris.Core.TT hiding (score)
2425import Idris.Core.Unify (match_unify)
2526import Idris.Delaborate (delab, delabTy)
2627import Idris.Docstrings (noDocs, overview)
@@ -54,7 +55,7 @@ searchByType h pterm = do
5455 syn = defaultSyntax { implicitAllowed = True } -- syntax
5556 n = sMN 0 "searchType" -- name
5657
57−
58+-- | Conduct a type-directed search using a given match predicate
5859searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
5960searchUsing pred istate ty =
6061 concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
@@ -64,7 +65,6 @@ searchUsing pred istate ty =
6465 guard $ not (special k)
6566 y <- get (fst4 x)
6667 let ny = normaliseC ctxt [] y
67− -- traceShow k False `seq` return ()
6868 val <- pred istate nty ny
6969 return (y, val)
7070 nty = normaliseC ctxt [] ty
@@ -77,45 +77,54 @@ searchUsing pred istate ty =
7777 get (CaseOp _ ty _ _ _ _) = Just ty
7878 get _ = Nothing
7979 special :: Name -> Bool
80+ special (NS n ns) = special n
8081 special (SN _) = True
82+ special (UN n) = T.pack "default#" `T.isPrefixOf` n
8183 special _ = False
8284
83−
84−tcToMaybe :: TC' e a -> Maybe a
85−tcToMaybe (OK x) = Just x
86−tcToMaybe (Error _) = Nothing
87−
88−
89−
85+-- Our default search predicate.
9086searchPred :: IState -> Type -> Type -> Maybe Score
9187searchPred istate ty1 = \ty2 -> case matcher ty2 of
92− Nothing -> Nothing
93− Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
88+ xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
9489 where
95− matcher = unifyWithHoles True istate ty1
96−
90+ matcher = unifyWithHoles istate ty1
9791
9892
93+typeFromDef :: (Def, b, c, d) -> Maybe Type
94+typeFromDef (def, _, _, _) = get def where
95+ get :: Def -> Maybe Type
96+ get (Function ty tm) = Just ty
97+ get (TyDecl _ ty) = Just ty
98+ -- get (Operator ty _ _) = Just ty
99+ get (CaseOp _ ty _ _ _ _) = Just ty
100+ get _ = Nothing
99101
100102reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
101103reverseDag xs = map f xs where
102104 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)
103105
104106-- run vToP first!
107+-- | Compute a directed acyclic graph corresponding to the
108+-- arguments of a function.
105109-- returns [(the name and type of the bound variable
106110-- the names in the type of the bound variable)]
107−computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)
108−computeDagP t = (reverse (map f args), retTy) where
109−
111+computeDagP :: Ord n
112+ => (TT n -> Bool) -- ^ filter to remove some arguments
113+ -> TT n
114+ -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
115+computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
110116 f (n, t) = ((n, t), M.keysSet (usedVars t))
111117
112− (numArgs, args, retTy) = go 0 [] t
118+ (numArgs, args, removedArgs, retTy) = go 0 [] [] t
113119
114120 -- NOTE : args are in reverse order
115− go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc
116− go k args retTy = (k, args, retTy)
117−
121+ go k args removedArgs (Bind n (Pi t) sc) = let arg = (n, t) in
122+ if removePred t
123+ then go k args (arg : removedArgs) sc
124+ else go (succ k) (arg : args) removedArgs sc
125+ go k args removedArgs retTy = (k, args, removedArgs, retTy)
118126
127+-- | Collect the names and types of all the free variables
119128usedVars :: Ord n => TT n -> Map n (TT n)
120129usedVars (V j) = error "unexpected! run vToP first"
121130usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t
@@ -133,6 +142,8 @@ deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
133142 then id
134143 else (((name2, ty) , (ix, S.delete name set)) :) ) (deleteFromDag name xs)
135144
145+deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
146+deleteFromArgList n = filter ((/= n) . fst)
136147
137148data Score = Score
138149 { transposition :: Int
@@ -143,17 +154,17 @@ data Score = Score
143154
144155displayScore :: Score -> Doc a
145156displayScore (Score trans lapp rapp lclass rclass) = text $ case (lt, gt) of
146− (True , True ) -> "="
147− (True , False) -> "<"
148− (False, True ) -> ">"
157+ (True , True ) -> "=" -- types are isomorphic
158+ (True , False) -> "<" -- found type is more general than searched type
159+ (False, True ) -> ">" -- searched type is more general than found type
149160 (False, False) -> " "
150161 where lt = lapp + lclass == 0
151162 gt = rapp + rclass == 0
152163
153164
154165scoreCriterion :: Score -> Bool
155−scoreCriterion (Score a b c d e) = True {- not
156− ( (b > 0 && c > 0) || (b + c) > 2 ) -}
166+scoreCriterion (Score a b c d e) = not
167+ ( (b > 0 && c > 0) || (b + c) > 4 || d > 3 || e > 3 )
157168
158169defaultScoreFunction :: Score -> Int
159170defaultScoreFunction (Score a b c d e) = a + 9*b + 3*c + 12*d + 4*e + 100*(2*b + d)*(2*c + e)
@@ -163,141 +174,184 @@ instance Monoid Score where
163174 mempty = Score 0 0 0 0 0
164175 (Score a b c d e) `mappend` (Score a' b' c' d' e') = Score (a + a') (b + b') (c + c') (d + d') (e + e')
165176
166−
177+-- | A directed acyclic graph representing the arguments to a function
178+-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
167179type ArgsDAG = [((Name, Type), (Int, Set Name))]
168−type ResType = ( [Name] , ArgsDAG , ArgsDAG )
169180
181+-- | The state corresponding to an attempted match of two types.
170182data State = State
171− { holes :: ![Name]
172− , args1 :: !ArgsDAG
173− , args2 :: !ArgsDAG
174− , score :: !Score
175− }
183+ { holes :: ![Name] -- ^ names which have yet to be resolved
184+ , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved
185+ , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved
186+ , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved
187+ , classes2 :: ![(Name, Type)] -- ^ typeclass arguments for the right type which haven't been resolved
188+ , score :: !Score -- ^ the score so far
189+ , usedNames :: ![Name] -- ^ all names that have been used
190+ } deriving Show
191+
192+modifyTypes :: (Type -> Type) -> State -> State
193+modifyTypes f (State h a1 a2 c1 c2 s un) =
194+ State h (modifyDag a1) (modifyDag a2)
195+ (modifyList c1) (modifyList c2)
196+ s un
197+ where
198+ modifyDag = map (first (second f))
199+ modifyList = map (second f)
200+
201+findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
202+findNameInArgsDAG name xs = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst) $ xs
203+
204+findLeft, findRight :: Name -> State -> Maybe (Type, Maybe Int)
205+findLeft n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a1 <|> ((,) <$> lookup n c1 <*> Nothing)
206+findRight n (State _ a1 a2 c1 c2 _ _) = findNameInArgsDAG n a2 <|> ((,) <$> lookup n c2 <*> Nothing)
207+
208+deleteLeft, deleteRight :: Name -> State -> State
209+deleteLeft n state = state { args1 = deleteFromDag n (args1 state) , classes1 = filter ((/= n) . fst) (classes1 state) }
210+deleteRight n state = state { args2 = deleteFromDag n (args2 state) , classes2 = filter ((/= n) . fst) (classes2 state) }
211+
212+
213+tcToMaybe :: TC' e a -> Maybe a
214+tcToMaybe (OK x) = Just x
215+tcToMaybe (Error _) = Nothing
216+
217+inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
218+inArgTys = map . first . second
176219
177220
178221--DONT run vToP first!
179−unifyWithHoles :: Bool -> IState -> Type -> Type -> Maybe [Score]
180−unifyWithHoles debugParam istate type1 = \type2 -> let
181− (dag2, retTy2) = makeDag (uniqueBinders argNames1 type2)
222+-- | Try to match two types together in a unification-like procedure.
223+-- Returns a list of possible scores representing ways in which the two
224+-- types can be matched.
225+unifyWithHoles :: IState -> Type -> Type -> [Score]
226+unifyWithHoles istate type1 = \type2 -> let
227+ (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
182228 argNames2 = map (fst . fst) dag2
183229 startingHoles = argNames1 ++ argNames2
184230
185231 startingTypes = (retTy1, retTy2) : []
186− in do
187− state <- go (State startingHoles dag1 dag2 mempty) startingTypes
188− return $ processDags state
232+ in case unifyQueue (State startingHoles dag1 dag2
233+ typeClassArgs1 typeClassArgs2
234+ mempty startingHoles) startingTypes
235+ of Nothing -> []
236+ Just state -> possibleMatches state
189237 where
190238 ctxt = tt_ctxt istate
191239 classInfo = idris_classes istate
192− (dag1, retTy1) = makeDag type1
193− argNames1 = map (fst . fst) dag1
194− makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP
195240
196− matchf :: (Name, Term) -> Maybe (Name, Name)
197− matchf (name, P Bound name2 _) = Just (name, name2)
198− matchf _ = Nothing
241+ isTypeClassArg :: Type -> Bool
242+ isTypeClassArg ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
243+ (clss, args) = unApply ty
244+ getClassName (P (TCon _ _) className _) = [className]
245+ getClassName _ = []
246+
247+ (dag1, typeClassArgs1, retTy1) = makeDag type1
248+ argNames1 = map (fst . fst) dag1
249+ makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
250+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP
251+ first3 f (a,b,c) = (f a, b, c)
199252
200253 -- update our state with the unification resolutions
201− updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)
202− updateDags [] res = Just (res, [], mempty)
203− updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) | isJust findArgs = do
254+ resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
255+ resolveUnis [] state = Just (state, [])
256+ resolveUnis ((name, term@(P Bound name2 _)) : xs)
257+ state@(State holes args1 args2 _ _ _ _) | isJust findArgs = do
204258 ((ty1, ix1), (ty2, ix2)) <- findArgs
205259
206− (res, queue, score) <- updateDags xs (holes', args1'', args2'')
207− --traceShow (ty1, ty2) False `seq` return ()
208− return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })
260+ (state'', queue) <- resolveUnis xs state'
261+ let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
262+ return $ (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
209263 where
210− findArgs = ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>
211− ((,) <$> mgetType name2 args1 <*> mgetType name args2)
264+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
265+ inScore f state = state { score = f (score state) }
266+ findArgs = ((,) <$> findLeft name state <*> findRight name2 state) <|>
267+ ((,) <$> findLeft name2 state <*> findRight name state)
212268 matchnames = [name, name2]
213269 holes' = holes \\ matchnames
214− substf = deleteFromDag name . deleteFromDag name2
215− args1' = substf args1
216− args2' = substf args2
217− args1'' = map (first . second $ subst name term) args1'
218− args2'' = map (first . second $ subst name term) args2'
219− mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
220−
221− updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of
222− (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep
223− (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep
270+ deleteArgs = deleteLeft name . deleteLeft name2 . deleteRight name . deleteRight name2
271+ state' = modifyTypes (subst name term) $ deleteArgs
272+ (state { holes = holes'})
273+
274+ resolveUnis ((name, term) : xs)
275+ state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
276+ (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep
277+ (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
224278 (Nothing, Nothing) -> nextStep
225279 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
226280 where
227− varsInTy = map fst $ M.toList (usedVars term)
228− deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)
229− thrd f (a,b,c) = (a,b,f c)
230− nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )
231− updatef = map (first . second $ subst name term) . deleteMany
232− mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs
233−
234−
235− go :: State -> [(Type, Type)] -> Maybe State
236− --go (State holes args1 args2 score) queue | trace ("go\n\t" ++ show holes ++ "\n\t" ++ show args1 ++ "\n\t" ++ show args2 ++ "\n\t" ++ show queue) False = undefined
237− go state [] = return state
238− go (State holes args1 args2 score) ((ty1, ty2) : queue) = do
239− res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] holes []
240− --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()
241− --guard (null errors)
242− ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)
243− let newScore = score `mappend` scoreAdditions
244− guard $ scoreCriterion newScore
245− go (State holes' args1' args2' newScore) (queue ++ queueAdditions)
246−
247−
248− processDags :: State -> [Score]
249− processDags (State [] [] [] scoreAcc) = [scoreAcc]
250− --processDags (State holes (_:_) [] scoreAcc) = []
251− --processDags (State holes [] (_:_) scoreAcc) = []
252− processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- allResults ] where
253−
254− results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)
255− (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]
256− | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]
257−
258− results2 = [ State (holes \\ [nameOf ty])
259− (deleteFromDag (nameOf ty) dag1) dag2
260− (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
261− | ty <- typeClassArgs1 ]
262−
263− typeClassArgs1 = filter (isSaturatedClass . typeOf) dag1
264− typeClassArgs2 = filter (isSaturatedClass . typeOf) dag2
265−
266−
267− results3 = [ State (holes \\ [nameOf ty])
268− dag1 (deleteFromDag (nameOf ty) dag2)
269− (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
270− | ty <- typeClassArgs2 ]
271−
272− allResults :: [State]
273− allResults = {- (if not (null typeClasses) then (traceShow typeClasses False `seq` id) else id ) -}
274− (results ++ results2 ++ results3)
275− where
276− typeClasses = filter (isSaturatedClass . typeOf) (dag1 ++ dag2)
277−
278−
279− -- check if the canBeFirst thing is losing any possibilities
280−
281−
282− inArgTys = map . first . second
283− typeOf ((name, ty), set) = ty
284− nameOf ((name, ty), set) = name
285−
286− -- XXX : debug stuff
287− canBeFirst = if debugParam then filter (S.null . snd . snd) else id
288− holes = map (fst . fst) dag1 ++ map (fst . fst) dag2
289−
290− deleteIdx _ [] = []
291− deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs
292−
293− isSaturatedClass :: Type -> Bool
294− isSaturatedClass ty = fromMaybe False $ do
281+ inScore f state = state { score = f (score state) }
282+ state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $
283+ state { holes = holes \\ [name]}
284+ nextStep = resolveUnis xs state'
285+
286+
287+ -- | resolve a queue of unification constraints
288+ unifyQueue :: State -> [(Type, Type)] -> Maybe State
289+ unifyQueue state [] = return state
290+ unifyQueue state ((ty1, ty2) : queue) = do
291+ res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []
292+ (state', queueAdditions) <- resolveUnis res state
293+ guard $ scoreCriterion (score state')
294+ unifyQueue state' (queue ++ queueAdditions)
295+
296+ possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]
297+ possClassInstances usedNames ty = do
295298 className <- getClassName clss
296− let possInstances = concatMap class_instances $ lookupCtxt className classInfo
297− return $ (SN (sInstanceN className (map argToName args))) `elem` possInstances
299+ classDef <- lookupCtxt className classInfo
300+ n <- class_instances classDef
301+ def <- lookupCtxt n (definitions ctxt)
302+ ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
303+ let ty' = vToP (uniqueBinders usedNames ty)
304+ return (getArgTys ty', getRetTy ty')
298305 where
299306 (clss, args) = unApply ty
300− getClassName (P (TCon _ _) className _) = Just className
301− getClassName _ = Nothing
302− argToName arg = show (delab istate arg)
307+ getClassName (P (TCon _ _) className _) = [className]
308+ getClassName _ = []
309+
310+ -- | Find all possible matches starting from a given state.
311+ possibleMatches :: State -> [Score]
312+ possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
313+ possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =
314+ concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where
315+
316+ -- we only try to match arguments whose names don't appear in the types
317+ -- of any other arguments
318+ canBeFirst :: ArgsDAG -> [(Name, Type)]
319+ canBeFirst = map fst . filter (S.null . snd . snd)
320+
321+ -- this is done rather than concatenating all three results in hopes of narrowing
322+ -- the search tree
323+ results = fromMaybe [] $ find (not . null) [results1, results2, results3]
324+
325+ -- try to match an argument from the left with an argument from the right
326+ results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)
327+ ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
328+ | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
329+
330+ -- try to match a typeclass argument from the left with a typeclass argument from the right
331+ results2 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) dag1 (inArgTys subst2for1 dag2)
332+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
333+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
334+
335+ -- try to hunt match a typeclass constraint by replacing it with an instance
336+ results3 = if null dag1 || null dag2 then catMaybes (results3A ++ results3B) else []
337+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
338+ noDeps (n, ty) = ((n, ty), (0, S.empty))
339+ results3A = [ unifyQueue
340+ (State ((holes \\ [n]) ++ newHoles) (dag1 ++ map noDeps newNonClassArgs) dag2
341+ (deleteFromArgList n c1 ++ newClassArgs) c2
342+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
343+ (usedNames ++ newHoles)
344+ )
345+ [(ty, inst)]
346+ | ((n, ty), (newArgs, inst)) <- typeClassArgs c1, let newHoles = map fst newArgs
347+ , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
348+ results3B = [ unifyQueue
349+ (State ((holes \\ [n]) ++ newHoles) dag1 (dag2 ++ map noDeps newNonClassArgs)
350+ c1 (deleteFromArgList n c2 ++ newClassArgs)
351+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
352+ (usedNames ++ newHoles)
353+ )
354+ [(ty, inst)]
355+ | ((n, ty), (newArgs, inst)) <- typeClassArgs c2, let newHoles = map fst newArgs
356+ , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
303357