5ffef89 · Idris-dev · git.iko.soy

src/Idris/Core/TT.hs+3−2

compare with master

unifiedsplit

@@ -196,8 +196,9 @@ score _ = 0

196instance Show Err where

197 show (Msg s) = s

198 show (InternalMsg s) = "Internal error: " ++ show s

199− show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

199+ show (CantUnify rec l r e sc i) = "CantUnify " ++ show rec ++ " " ++

200+ show l ++ " " ++ show r ++ " " ++

200− ++ show e ++ " in " ++ show sc ++ " " ++ show i

201+ show e ++ " in " ++ show sc ++ " " ++ show i

201 show (CantSolveGoal g _) = "CantSolve " ++ show g

202 show (CantSolveGoal g _) = "CantSolve " ++ show g

202 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

203 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

203 show (ProviderError msg) = "Type provider error: " ++ msg

204 show (ProviderError msg) = "Type provider error: " ++ msg

src/Idris/Core/Unify.hs+14−1

@@ -1,6 +1,7 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..)) where

3+module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..),

4+ unrecoverable) where

4

5

5import Idris.Core.TT

6import Idris.Core.TT

6import Idris.Core.Evaluate

7import Idris.Core.Evaluate

@@ -30,6 +31,16 @@ data FailContext = FailContext { fail_sourceloc :: FC,

30type Injs = [(TT Name, TT Name, TT Name)]

31type Injs = [(TT Name, TT Name, TT Name)]

31type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

32type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

32

33

34+unrecoverable :: Fails -> Bool

35+unrecoverable = any bad

36+ where bad (_,_,_, err, _, _) = unrec err

37+

38+ unrec (CantUnify r _ _ _ _ _) = not r

39+ unrec (At _ e) = unrec e

40+ unrec (Elaborating _ _ e) = unrec e

41+ unrec (ElaboratingArg _ _ _ e) = unrec e

42+ unrec _ = False

43+

33data UInfo = UI Int Fails

44data UInfo = UI Int Fails

34 deriving Show

45 deriving Show

35

46

@@ -628,6 +639,8 @@ recoverable p@(Constant _) (App f a) = recoverable p f

628recoverable (App f a) p@(Constant _) = recoverable f p

639recoverable (App f a) p@(Constant _) = recoverable f p

629recoverable p@(P _ n _) (App f a) = recoverable p f

640recoverable p@(P _ n _) (App f a) = recoverable p f

630recoverable (App f a) p@(P _ _ _) = recoverable f p

641recoverable (App f a) p@(P _ _ _) = recoverable f p

642+recoverable (App f a) (App f' a')

643+ | f == f' = recoverable a a'

631recoverable (App f a) (App f' a')

644recoverable (App f a) (App f' a')

632 = recoverable f f' -- && recoverable a a'

645 = recoverable f f' -- && recoverable a a'

633recoverable f (Bind _ (Pi _) sc)

646recoverable f (Bind _ (Pi _) sc)

src/Idris/ElabTerm.hs+2−1

@@ -1025,7 +1025,8 @@ resTC' tcs depth topg fn ist

1025 args <- map snd <$> try' (apply (Var n) imps)

1026 (match_apply (Var n) imps) True

1027 ps' <- get_probs

1028+ when (length ps < length ps' || unrecoverable ps') $

1028− when (length ps < length ps') $ fail "Can't apply type class"

1029+ fail "Can't apply type class"

1029-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1030-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1030 mapM_ (\ (_,n) -> do focus n

1031 mapM_ (\ (_,n) -> do focus n

1031 t' <- goal

1032 t' <- goal