Currently, the type system of Gobra disallows array literals like [3]int{} from occurring in strongly pure contexts, even though an array is a value type (similarly to structs). Furthermore, the type system (wrongly) allows slice and map literals in pure contexts, even though it shouldn't because slices and maps are reference types. This PR addresses this classification.
To implement this, I had to fix the function underlyingTypeWithCtxP to allow for ADTs
Currently, the type system of Gobra disallows array literals like
[3]int{}from occurring in strongly pure contexts, even though an array is a value type (similarly to structs). Furthermore, the type system (wrongly) allows slice and map literals in pure contexts, even though it shouldn't because slices and maps are reference types. This PR addresses this classification.To implement this, I had to fix the function
underlyingTypeWithCtxPto allow for ADTs