Agda infers an incorrect type with subtyping on

[liesnikov]

As per title, with a subtyping flag on, Agda doesn't infer the right type. Example in question:

{-# OPTIONS --subtyping #-}
module Example where
  private
    variable
      A : Set
      B : Set
  
  -- the usual type
  -- const : A → B → A
  -- but we can mark the second argument as irrelevant
  const : A → .B → A
  const x = λ _ → x
  
  record Ex (F : Set → Set) :
                 Set₁ where
    infixl 4 _<$>_
  
    field
      _<$>_ : (A → B) → F A → F B
  
    -- this is going to blow up because the type of
    -- (const <$>) is F A → F (.B → A)
    -- and not F A → F (B → A)
    -- the latter two don't match since we don't know whether (an abstract)
    -- F is co- or contra-variant
    ex : F A → F (B → A)
    ex x = const <$> x
    -- this works though
    --  ex {A = A} {B = B} x = _<$>_ {A = A} {B = B → A} (const {A} {B}) x
    -- this works too
    -- ex = _<$>_ const

@jespercockx and I tried a naïve fix (f78b8c1) which eliminates the shortcuts if the subtyping flag is on. However, with these changes one gets an unsolved meta error with the following constraints:

Failed to solve the following constraints:
  _A_24 =< A (blocked on _A_24)
  B =< _B_25 (blocked on _B_25)
  A =< _A_24 (blocked on _A_24)
Unsolved metas at the following locations:
  /home/bohdan/delft/agda/agda/Example.agda:28,12-17

[jespercockx]

Note that we have some special heuristics for inequalities between universe levels that are used to simplify the analogous inequalities between levels, see https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/LevelConstraints.hs

However, even if these heuristics were applied more generally to types, this would only solve the first and third constraint, leaving the second one B =< _B_25. Indeed, with subtyping there is no reason to believe that the type should be precisely B; it could be any supertype. So it seems that subtyping requires us to choose between two inconvenient options:

• Solve some metavariables with non-unique solutions (e.g. _B_25 := B in the above example, see also the "default to infinity" rule for sized types and the "default to zero" rule for universe levels).
• Accept that many metavariables that can be solved without subtyping cannot be solved anymore with it, and hence need to be given explicitly.

Summoning @andreasabel and @flupe to ask if they have any additional insights.

[andreasabel]

Fixed by:

• [ #5427 ] Removed support for subtyping for erasure and irrelevance. #5608