search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

"If the news bulletin defines this hole, it had better just be hoping for a solution" #53

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
In Elaboration.Wire, on:

> tellEntry news (EDEF  ref@(name := HOLE h :<: tyv) sn
>                       dkind dev@(Dev {devTip=Suspended tt prob}) ty)
>   | Just ne <- getNews news ref = do

The documentation states that "If the news bulletin defines this hole, it had 
better just be hoping for a solution". This is enforced by the following code:

>      case prob of
>       ElabHope  -> tellEntry news (EDEF ref sn dkind (dev{devTip=Unknown tt}) 
ty)
>       _         -> throwError' (...)

My question is: is this an invariant we are supposed to enforce? Or it's 
something the user could break? In the former case, this must be an |error|, 
not a |throwError|. In the latter case, I'm afraid the user will be rather 
confused if this error were to happen for real.

Original issue reported on code.google.com by pedag...@gmail.com on 26 Aug 2010 at 10:17