Typechecking infers incorrect types

[lukaszcz]

Input:

module ty1;

import Stdlib.Prelude open;

trait
type Functor (f : Type -> Type) :=
  mkFunctor {
    fmap : {A B : Type} -> (A -> B) -> f A -> f B
  };

instance
listFunctorI : Functor List :=
  mkFunctor@{
    fmap := map;
  };

Output after running uvix dev internal typecheck ty1.juvix --print-result --new-typechecker:

import Stdlib.Prelude

mutual {
  listFunctorI : Functor List
    := let 
      not-mutual fmap : (f : A → B) → List A → List B
        := map {A} {B}
     in let 
      not-mutual f : Type → Type := List
      not-mutual fmap : {A : Type} → {B : Type} → (A → B) → f A → f B
        := λ {| {_ω1276} {_ω1277} := fmap}
     in mkFunctor {f} fmap

  type Functor (f : Type → Type) =
    mkFunctor : (fmap : {A : Type} → {B : Type} → (A → B) → f A → f B) → Functor f
}

mutual fmap : {f : Type → Type} → {{Functor f}} → {A : Type} → {B : Type} → (A → B) → f A → f B
  := λ : {f : Type → Type} → {{Functor f}} → {A : Type} → {B : Type} → (A → B) → f A → f B {| {_ω1282} ({{(mkFunctor a : Functor _ω1282)}}) {_ω1283} {_ω1284} := a {A} {B}}

In the fist fmap, the type variables A and B are not bound, which later makes the translation from Internal to Core fail.

[lukaszcz]

This is actually a bug with the new named arguments syntax. Just before having type constructor parameters for inductive types we never used type variables in constructors.

[lukaszcz]

Well, the bug is in the typechecker, both the new and old one, the named arguments syntax only exposes it.

Running juvix dev internal pretty ty1.juvix --new-typechecker results in:

mutual {
  listFunctorI : Functor List
    := let 
      not-mutual fmap : _ := map
     in let 
      not-mutual f : Type → Type := _
      not-mutual fmap : {A : Type} → {B : Type} → (A → B) → f A → f B
        := fmap
     in mkFunctor {f} fmap

  type Functor (f : Type → Type) =
    mkFunctor : (fmap : {A : Type} → {B : Type} → (A → B) → f A → f B) → Functor f
}

This is still correct. The holes are incorrectly inferred, without taking scope into account.

[lukaszcz]

For the old typechecker, the following input exposes the bug:

module ty2;

import Stdlib.Prelude open;

trait
type Functor (F : Type) :=
  mkFunctor {
    fmap : {A : Type} -> (A -> A) -> F -> F
  };

fmapLst {A} (f : A -> A) (l : List Nat) : List Nat := l;

instance
listFunctorI : Functor (List Nat) :=
  mkFunctor@{
    fmap := fmapLst;
  };

[lukaszcz]

@janmasrovira can you look at this? Is there some easy fix or this exposes a bigger issue with holes having no context?

[lukaszcz]

A simpler example without traits:

module ty3;

id0 : {A : Type} -> A -> A :=
  let id : _ := λ{x := x};
      id' : {A : Type} -> A -> A := id
  in id';

Running juvix dev internal typecheck ty3.juvix --print-result gives:

mutual id0 : {A : Type} → A → A
  := let 
    not-mutual id : _ω8 → _ω8 := λ : _ω8 → _ω8 {| x := x}
    not-mutual id' : {A : Type} → A → A
      := λ : {A : Type} → A → A {| {_ω8} := id}
   in id'

Running juvix typecheck ty3.juvix results in:

juvix: impossible
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base.hs:392:14 in juvix-0.5.3-6xl5bc4fEBjCQTOL6knJUZ:Juvix.Prelude.Base
  impossible, called at src/Juvix/Compiler/Core/Translation/FromInternal.hs:859:34 in juvix-0.5.3-6xl5bc4fEBjCQTOL6knJUZ:Juvix.Compiler.Core.Translation.FromInternal

[lukaszcz]

It seems like the problem is with not remembering the hole context.

[janmasrovira]

this could be related or the exact same problem as #2247

[lukaszcz]

I guess we need to fix this before making use of type constructor inductive parameters. This bug gets exposed whenever there are record fields with implicit type arguments, which happens with Functor and so on. A workaround is to explicitly annotate the types of all such fields in record construction or don't use the named arguments syntax in such cases, but this is not acceptable. The translation from Internal to Core seems to work with the new typechecker with these workarounds.

[janmasrovira]

The original problem reported in this issue has been solved in #2524.

The #2247 problem still remains but I'm closing this to avoid duplicates.