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

git.iko.soy/Idris-dev

Type class resolution fix

Check whether any errors introduced by a match are unrecoverable, rather than merely checking if any more errors are introduced. Otherwise, in some circumstances (where other problems are resolved by the match) we might get a type class resolved where it shouldn't be, leading to mysterious errors later. Fixes #1365

commit5ffef8982e53ece8f02abbae8ec18e0fb4fea596 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 8 Jul 2014, 12:25 (12 years ago) parente363c09

3 files changed+19−4

compare with master

unifiedsplit

src/Idris/Core/TT.hs+3−2 src/Idris/Core/Unify.hs+14−1 src/Idris/ElabTerm.hs+2−1

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

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

196196instance Show Err where

197197 show (Msg s) = s

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

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

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

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

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

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

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

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

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

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

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

11{-# LANGUAGE PatternGuards #-}

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

56import Idris.Core.TT

67import Idris.Core.Evaluate

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

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

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

3233

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+

3344data UInfo = UI Int Fails

3445 deriving Show

3546

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

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

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

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

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

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

631644recoverable (App f a) (App f' a')

632645 = recoverable f f' -- && recoverable a a'

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

src/Idris/ElabTerm.hs+2−1

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

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

10261026 (match_apply (Var n) imps) True

10271027 ps' <- get_probs

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

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

1029+ fail "Can't apply type class"

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

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

10311032 t' <- goal