Subtyping failure for pure/impure functions under type constructors

The interpreter currently treats type constructors like `List` and `Option` as invariant with respect to function purity. While a total function (`->`) is correctly treated as a subtype of an impure function (`->>`) in isolation, it does not recognize it correctly when nested inside a constructor as shown in the following REPL session.

```ml
> let id (x : Int) = x ;;
> id ;;
: Int -> Int
=
> let rec factorial (x : Int) = if x == 0 then 1 else x * (factorial (x-1)) ;;
> factorial ;;
: Int ->[] Int
=
> let xs = [id, factorial] ;;
error: This expression has type List (Int ->> Int), but an expression was expected of type List (Int -> Int)
| let xs = [id, factorial] ;;
| ^^^^^^^^^^
|
> let ys = [factorial, id] ;;
error: This expression has type List (Int -> Int), but an expression was expected of type List (Int ->> Int)
| let ys = [factorial, id] ;;
| ^^^
|
> let (x : Option (Int ->> Int)) = Some id ;;
error: Annotating pattern with type Option (Int ->> Int), but it was expected to match values of type Option (Int -> Int)
| let (x : Option (Int ->> Int)) = Some id ;;
| ^^^^^^^^^^^^^^^^^^^^
|
> let (x : Option (Int ->> Int)) = Some (id : Int ->> Int) ;;
>
```

It is possible to circumvent that problem by explicitly annotating the value under the constructor with the supertype, but it would be nice if the interpreter did it automatically.
```ml
> let zs = [factorial, (id : Int ->> Int)] ;;
> let (y : Option (Int ->> Int)) = Some (id : Int ->> Int) ;;
>
```

Start by reproducing the List and Option examples in the issue's REPL session, then trace the interpreter's subtype checking for function purity under type constructors. Done means the examples accept pure functions where impure functions are expected without explicit annotations, while preserving the existing standalone function-subtyping behavior.

Written by the indexing model from the issue text.