ModuleSystemMoreFlexible

This does not type check:

  module Annoying where

  data A : Set where
    a₁ : A
    a₂ : A

  data B : A -> Set where
    b₁ : B a₁
    b₂ : B a₂

  module M (a : A) where

    id : B a -> B a
    id b₁ = b₁
    id b₂ = b₂

The reason is that the parameter a to M is fixed when id is type checked, so it cannot be instantiated to a₁ or a₂. This can be annoying, and the workaround is to inline the module M (or distribute the parameter a to all functions in M), which makes the code less modular. Hence I suggest that the type checker should be more flexible, so that it can handle this example.