Skip to content

Draft: checkEqForallVis

Vladislav Zavialov requested to merge wip/int-index/visibility-check into master

Prior to this change, the equality relation on types took ForAllTyFlag into account, making a distinction between:

  1. forall a. blah
  2. forall a -> blah

Not anymore.

This distinction is important in surface Haskell, but it has no meaning in Core where type abstraction and type application are always explicit. At the same time, if we are not careful to track this flag, Core Lint will fail, as reported in #22762 (closed):

*** Core Lint errors : in result of TcGblEnv axioms ***
From-kind of Cast differs from kind of enclosed type
From-kind: forall (b :: Bool) -> *
Kind of enclosed type: forall {b :: Bool}. *

The solution is to compare types for equality modulo visibility (ForAllTyFlag). Updated functions:

  • nonDetCmpType (worker for eqType)
  • eqDeBruijnType
  • tc_eq_type (worker for tcEqType)
  • can_eq_nc

In order to retain the distinction between visible and invisible forall in user-written code, we introduce a new ad-hoc check: checkEqForallVis.

Edited by Vladislav Zavialov

Merge request reports