mbenke / hm-typecheck

Experimental typechecker for a Solidity intermediate language
3 stars 1 forks source link

Miscompilation of examples/mona/03join.fun to Yul #5

Closed mbenke closed 4 months ago

mbenke commented 4 months ago

examples/mona/03join.fun

type Option[a] = None | Some[a];
just x = Some x;
maybe n o = case o of { None -> n; Some x -> x };
join mmx = case mmx of {
    None -> None;
    Some mx -> case mx of {
      None -> None;
      Some x -> Some x }
};
main = maybe 7 (join(Some (Some 42)));

Expected: 42, actual: 7

Core:

function join$Int (mmx : (unit + (unit + int))) -> (unit + int) {
  let _caseresult : (unit + int)
  match mmx with
  { inl left => _caseresult := inl(())
    inr right => {   let _caseresult : (unit + int)
                     match right with
                     { inl left => _caseresult := inl(())
                       inr right => _caseresult := inr(right)
                     }
                     _caseresult := _caseresult
                 }
  }
  return _caseresult
}
function main () -> int {
  return maybe$Int(7, join$Int(inr(inr(42))))
}
function maybe$Int (n : int, o : (unit + int)) -> int {
  let _caseresult : int
  match o with
  { inl left => _caseresult := n
    inr right => _caseresult := right
  }
  return _caseresult
}

(seems correct except for superfluous _caseresult := _caseresult)

mbenke commented 4 months ago

Actually the core is wrong: we have two different case results, so join should be:

function join$Int (mmx : (unit + (unit + int))) -> (unit + int) {
  let _caseresult1 : (unit + int)
  match mmx with
  { inl left => _caseresult1 := inl(())
    inr right => {   let _caseresult2 : (unit + int)
                     match right with
                     { inl left => _caseresult2 := inl(())
                       inr right => _caseresult2 := inr(right)
                     }
                     _caseresult1 := _caseresult2
                 }
  }
  return _caseresult1
}