Denis Buzdalov

`%runElab` and auto-delays go really crazy together

1

# Simple part ## Steps to Reproduce Try to typecheck ```idris import Language.Reflection %language ElabReflection scr : Elab Unit scr = fail "Show mustn't go on" vd : Lazy Unit...

Matching on an expression (when it's appropriate) fails when the expression is complex

1

# Context One can match an argument to a whole expression, if it matches with one: ```idris ff : (n, k : Nat) -> k = n + 1 ->...

Explicit dependent argument is not shadowed correctly in `where`-block

1

# Steps to Reproduce Consider the following function: ```idris genAtIndex : DecEq a => (n : Nat) -> (f : Fin n) -> (m : a) -> (v : Vect...

# Steps to Reproduce Consider a function that tries to use non-constructor expression when matching on the LHS: ```idris g : Nat -> Nat -> Nat g (x + 1)...

CSE optimisation is tough with `%inline` and lazy meeting in the same place

3

# Steps to Reproduce Run the following code: ```idris import Data.List.Lazy import Debug.Trace %default total %inline (::) : Maybe a -> Lazy (LazyList a) -> LazyList a Nothing :: xs...

`%defaulthint` works differently with `data` and `interface`

1

# Context You can use `%defaulthint` for `data` and it can be found with no problem even when it is a `auto`-parameter of some another hint: ```idris interface X where...

Unification tries to unify irrelevant things and fails to do so

1

# Steps to Reproduce This is a shrunk from a real code, so it lacks practicality, but still reveals strange behaviour. Consider the following definitions: ```idris data E = MkE...

# Steps to Reproduce Consider two variants of the same function: ```idris f : (n : Nat) -> (Void, Void) -> Nat f 0 (_, _) impossible f 1 (_,...

Quantity is lost when matching on a lazy value

3

`Lazy` values can be matched using `Delay`. But when `Lazy` value has unrestricted quantity, matched under `Delay` must have the same quantity. This usually holds, but when a value holding...

[ feature request ] Add support for alternative sources of package collections

1

I ran into a problem that some upstream package (which is not yet present in the pack collection) requires some additional or alternative versions of some packages, and thus downstream...