git.iko.soy/Idris-dev
on master help sign in
Fix universe checking error

Fixes #286. Constraints generated by the final convertibility check between lhs and rhs were not being added to the overall set!

commit2e6b5e08bbee646fcfaae7379998e29b0af23672 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 24 Dec 2014, 12:39 (12 years ago) parent73bad9f
3 files changed+11−4
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/Elab/Clause.hs+7−2 src/Idris/Error.hs+3−1
src/Idris/AbsSyntax.hs+1−1
@@ -493,7 +493,7 @@ addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
493493addConstraints fc (v, cs)
494494 = do i <- getIState
495495 let ctxt = tt_ctxt i
496− let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
496+ let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,
497497 next_tvar = v }
498498 let ics = zip cs (repeat fc) ++ idris_constraints i
499499 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
src/Idris/Elab/Clause.hs+7−2
@@ -41,6 +41,7 @@ import Control.Applicative hiding (Const)
4141import Control.DeepSeq
4242import Control.Monad
4343import Control.Monad.State.Strict as State
44+import qualified Control.Monad.State.Lazy as LState
4445import Data.List
4546import Data.Maybe
4647import Debug.Trace
@@ -695,8 +696,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
695696 then recheckC_borrowing True borrowed fc [] rhs'
696697 else return (rhs', clhsty)
697698 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
698− case converts ctxt [] clhsty crhsty of
699− OK _ -> return ()
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)
704+ return ()
700705 Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
701706 i <- getIState
702707 checkInferred fc (delab' i crhs True True) rhs
src/Idris/Error.hs+3−1
@@ -28,8 +28,10 @@ import qualified Data.Foldable as Foldable
2828
2929iucheck :: Idris ()
3030iucheck = do tit <- typeInType
31+ ist <- getIState
32+ let cs = idris_constraints ist
33+ logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs
3134 when (not tit) $
32− do ist <- getIState
3335 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
3436 (\e -> do setErrSpan (getErrSpan e)
3537 iputStrLn (pshow ist e))