2e6b5e0 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -493,7 +493,7 @@ addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

493addConstraints fc (v, cs)

494 = do i <- getIState

495 let ctxt = tt_ctxt i

496− let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,

496+ let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,

497 next_tvar = v }

498 let ics = zip cs (repeat fc) ++ idris_constraints i

499 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

src/Idris/Elab/Clause.hs+7−2

@@ -41,6 +41,7 @@ import Control.Applicative hiding (Const)

41import Control.DeepSeq

42import Control.Monad

43import Control.Monad.State.Strict as State

44+import qualified Control.Monad.State.Lazy as LState

44import Data.List

45import Data.List

45import Data.Maybe

46import Data.Maybe

46import Debug.Trace

47import Debug.Trace

@@ -695,8 +696,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

695 then recheckC_borrowing True borrowed fc [] rhs'

696 then recheckC_borrowing True borrowed fc [] rhs'

696 else return (rhs', clhsty)

697 else return (rhs', clhsty)

697 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

698 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

698− case converts ctxt [] clhsty crhsty of

699+ ctxt <- getContext

700+ let constv = next_tvar ctxt

701+ case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

702+ OK (_, cs) -> do addConstraints fc cs

703+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (constv,cs)

699− OK _ -> return ()

704+ return ()

700 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

705 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

701 i <- getIState

706 i <- getIState

702 checkInferred fc (delab' i crhs True True) rhs

707 checkInferred fc (delab' i crhs True True) rhs

src/Idris/Error.hs+3−1

@@ -28,8 +28,10 @@ import qualified Data.Foldable as Foldable

28

29iucheck :: Idris ()

30iucheck = do tit <- typeInType

31+ ist <- getIState

32+ let cs = idris_constraints ist

33+ logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs

31 when (not tit) $

34 when (not tit) $

32− do ist <- getIState

33 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

35 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

34 (\e -> do setErrSpan (getErrSpan e)

36 (\e -> do setErrSpan (getErrSpan e)

35 iputStrLn (pshow ist e))

37 iputStrLn (pshow ist e))