455ae60 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Attempt to resolve type classes before application

commit455ae604f522da0821d8bd333385d10a276b7868 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 28 Mar 2012, 23:18 (15 years ago) parente74e08d

3 files changed+10−3

unifiedsplit

src/Idris/AbsSyntax.hs+3−1

@@ -995,7 +995,9 @@ showImp impl tm = se 10 tm where

995995 where showbasic n@(UN _) = show n

996996 showbasic (MN _ s) = s

997997 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

998− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

998+ se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++

999+ (if impl then " : " ++ se 10 ty else "") ++ " => "

1000+ ++ se 10 sc

9991001 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

10001002 " in " ++ se 10 sc

10011003 se p (PPi (Exp l s) n ty sc)

src/Idris/Delaborate.hs+1

@@ -71,6 +71,7 @@ pshow i (Msg s) = s

7171pshow i (CantUnify x y e s)

7272 = "Can't unify " ++ show (delab i x)

7373 ++ " with " ++ show (delab i y) ++

74+-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

7475 case e of

7576 Msg "" -> ""

7677 _ -> "\n\nSpecifically:\n\t " ++ pshow i e

src/Idris/ElabTerm.hs+6−2

@@ -102,8 +102,12 @@ elab ist info pattern tcgen fn tm

102102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

103103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

104104 = resolveTC 5 fn ist

105− elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

106− instanceArg c

105+ elab' ina (PResolveTC fc)

106+ | pattern = do c <- unique_hole (MN 0 "c")

107+ instanceArg c

108+ | otherwise = try (resolveTC 2 fn ist)

109+ (do c <- unique_hole (MN 0 "c")

110+ instanceArg c)

107111 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

108112 pimp (MN 0 "x") Placeholder])

109113 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,