Opened 5 years ago

Last modified 17 months ago

#332 new bug

Type inference does not handle deBruijn variables.

Reported by: benl Owned by:
Priority: low Milestone:
Component: Core Type Checker Version: 0.4.1
Keywords: Cc:

Description

> :set lang Flow
ok
>
> :load..
module Test with letrec
x2runprocprocess [^ : Rate] (x2 : Vector# Bool#) (flags : Series# ^0 Bool#)
  = smkSel# [^0] flags
        (/\(k1 : Rate). \(sel : Sel1# ^0 k1).
         let x2s : Series# k1 Bool# = spack# sel flags in
             sfill# x2 x2s)
;;
Error loading module
  When checking expression.
    <console>:9:50
    Type mismatch.
      inferred type: Series# ^1 Bool#
      expected type: Series# ^0 ?5

    with: flags

Elimiating the deBruijn variable...

module Test with letrec
x2runprocprocess [k0 : Rate] (x2 : Vector# Bool#) (flags : Series# k0 Bool#)
  = smkSel# [k0] flags
        (/\(k1 : Rate). \(sel : Sel1# k0 k1).
         let x2s : Series# k1 Bool# = spack# sel flags in
             sfill# x2 x2s)
;;
module Test with
letrec {
  x2runprocprocess : [k0 : Rate].Vector# Bool# -> Series# k0 Bool# -> Process#
    = /\(k0 : Rate).
       \(x2 : Vector# Bool#).\(flags : Series# k0 Bool#).
      smkSel# [k0] flags
          (/\(k1 : Rate).
            \(sel : Sel1# k0 k1).
           let x2s : Series# k1 Bool# = spack# [k0] [k1] [Bool#] sel flags in
           sfill# [k1] [Bool#] x2 x2s)

Now it checks fine.

Change History (4)

comment:1 Changed 3 years ago by benl

  • Milestone 0.4.2 deleted

comment:2 Changed 3 years ago by benl

  • Summary changed from Type inference does not unify deBruijn variable. to Type inference does not handle deBruijn variables.

The region for 'letregion' also doesn't check for free indices in the body. There are likely similar problem in the other rules.

comment:3 Changed 2 years ago by benl

  • Priority changed from normal to low

comment:4 Changed 17 months ago by benl

  • Type changed from defect to bug
Note: See TracTickets for help on using tickets.