search

Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
217 stars 36 forks source link

FlowTypeCheck internal failure #1143

Open DavePearce opened 2 years ago

DavePearce commented 2 years ago

Test 001135 is this:

type neg is (int n) where n < 0
type pos is (int n) where n > 0

type exp1 is neg | {exp1 rest}
type exp2 is pos | {exp2 rest}

function f(exp1 e1) -> exp2:
    return (exp2) e1

This currently generates an internal failure:

wycc.lang.Syntactic$Exception
    at wyil.check.FlowTypeCheck.internalFailure(FlowTypeCheck.java:3486)
    at wyil.check.FlowTypeCheck.checkStatement(FlowTypeCheck.java:406)
    at wyil.check.FlowTypeCheck.checkBlock(FlowTypeCheck.java:330)
    at wyil.check.FlowTypeCheck.checkFunctionOrMethodDeclaration(FlowTypeCheck.java:272)
    at wyil.check.FlowTypeCheck.checkDeclaration(FlowTypeCheck.java:210)
    at wyil.check.FlowTypeCheck.checkUnit(FlowTypeCheck.java:223)
    at wyil.check.FlowTypeCheck.checkDeclaration(FlowTypeCheck.java:194)
    at wyil.check.FlowTypeCheck.check(FlowTypeCheck.java:182)