Kyle Ehrlich

contrib Data.Linear.Array is unsafe

15

You can easily get a linear vector outside of it's linear context like so: ``` unsafeMakeLinArray : (size : Int) -> LinArray t unsafeMakeLinArray size = newArray size (\x =>...

Multiplicity subtyping with dependent types can break linearity

2

# Steps to Reproduce ``` badEq : ((x: Nat) -> Nat) = ((1 x:Nat) -> Nat) badEq = Refl ``` # Expected Behavior The term should not typecheck because this...

### Describe the bug Arrow functions inside of getters use the `this` context of the surrounding context, rather than of the getter. ### Input code ```typescript const myObj = {...