f9c3fd9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change disambiguation rules back

It's too restrictive to require type class resolution early, especially for numeric types. For disambiguation to work, it needs a concrete type error in all but the successful branch. Tweak :exec to make it work under these rules.

commitf9c3fd9e67746f4d56b699620e23edebeddf55ec authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 5 Apr 2015, 18:43 (12 years ago) parentc3cdb9c

2 files changed+10−7

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+1−4 src/Idris/Elab/Value.hs+9−3

src/Idris/Core/Elaborate.hs+1−4

@@ -761,11 +761,8 @@ try' t1 t2 proofSearch

761761 ulog <- getUnifyLog

762762 ivs <- get_instances

763763 case prunStateT 999999 False ps t1 s of

764− OK ((v, _, _), s')

765− | length (instances (proof s')) <= length ivs ->

766− do put s'

764+ OK ((v, _, _), s') -> do put s'

767765 return $! v

768− | otherwise -> t2

769766 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

770767 if recoverableErr e1 then

771768 do case runStateT t2 s of

src/Idris/Elab/Value.hs+9−3

@@ -115,11 +115,17 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

115115 else Checked tm

116116 | otherwise = Unchecked

117117

118+-- Try running the term directly (as IO ()), then printing it as an Integer

119+-- (as a default numeric tye), then printing it as any Showable thing

118120elabExec :: FC -> PTerm -> PTerm

119121elabExec fc tm = runtm (PAlternative False

120− [PApp fc (PRef fc (sUN "printLn"))

121− [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp tm],

122− tm])

122+ [printtm (PApp fc (PRef fc (sUN "the"))

123+ [pexp (PConstant (AType (ATInt ITBig))), pexp tm]),

124+ tm,

125+ printtm tm

126+ ])

123127 where

124128 runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

129+ printtm t = PApp fc (PRef fc (sUN "printLn"))

130+ [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

125131