mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
26cfbe9e1e
If after an application there are more implicit arguments expected, add those arguments then re-elaborate the application - we often don't know what these arguments will be until after elaborating the application because the application itself may compute a type. Fixes #1899
15 lines
217 B
Idris
15 lines
217 B
Idris
%default total
|
|
|
|
InterpBool : () -> Type
|
|
InterpBool () = {x : Type} -> x -> Nat
|
|
|
|
class IdrisBug (u : ()) where
|
|
idrisBug : InterpBool u
|
|
|
|
instance IdrisBug () where
|
|
idrisBug _ = Z
|
|
|
|
f : Nat
|
|
f = idrisBug {u = ()} 'a'
|
|
|