Mark Barbone

Linear arguments and with clauses don't mix well

3

The compiler seems conflicted whether it would like linear arguments to be used in `with` clauses or not. ```idris pair : (1 _ : a) -> b -> (a, b)...

Feature request: try_insert method

1

The standard library hashmap and btree map [recently got a nightly-only `try_insert` operation](https://github.com/rust-lang/rust/pull/82764) ([here's the tracking issue](https://github.com/rust-lang/rust/issues/82766)), which makes it very convenient to insert something into a map, panicking in...

Performance issues with linear hashmap

7

The hashmap in `Data.HashMap.Mutable.Linear` is orders of magnitude slower than `Data.HashMap.Lazy` for large inputs. **To Reproduce** [I implemented the same code with both `Data.HashMap.Mutable.Linear` and `Data.HashMap.Lazy` in this gist](https://gist.github.com/mb64/5b0e662163617d8ea233668a48f5cd7e). On...

Unification failure

3

Hi! I've come across a strange issue, where this unification problem fails: `a:t -> F (G a) = X`. But if `X` is a ground term, it works. ```lpr Makam,...

Report delayed constraints in the REPL

2

When delayed higher-order unification problems remain unsolved, it would be useful to see the remaining constraints in the REPL. Currently, asking a query such as `eq (F 5) 5 ?`...

Strange behavior with `where` clauses in module signatures

2

**Scope:** I'm not sure whether this is an issue with SOSML or SOSML-frontend. Both behave strangely, but in different ways. **Description / To Reproduce:** Given this (valid) code ([SOSML editor...

Rename SDK version config labels

2

This was discussed a little in #223. It would be great to rename `android_version`, `min_sdk_version`, and `target_sdk_version` to a more coherent naming scheme. Some options could be: * `build_sdk_version`, `min_sdk_version`,...

# Steps to Reproduce ```idris x : Num a => Maybe a x = Just 1 y : Int y with (x) | Just n = n | Nothing =...

Structs are passed by pointer in FFI?

10

It seems to pass a `struct` via a pointer in an `extern "C"` function, instead of copying the value. I'm not sure if this is a bug in the AVR...

Unlike many common ISAs, MIPS has a [branch delay slot](https://en.wikipedia.org/wiki/Delay_slot#Branch_delay_slots) (see [this blog post](https://devblogs.microsoft.com/oldnewthing/20180411-00/?p=98485) for a better explanation in a MIPS specific context). The MIPS docs omits any mention of...