search

google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

bad type function accepted as inductively sequential #104

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
data Baz :: * ~> * ~> * where
  Quux :: Baz Int Int

bar :: * ~> *
{bar (a `Baz` b)} = a
{bar (Baz a b)} = a

prompt> :k bar
bar :: *0 ~> *0

Branchx [0] {bar a}
 Leaf {bar (Baz b c)} --> b
 Leaf {bar (Baz d e)} --> d

But the two leaves are alpha-equivalent!

Original issue reported on code.google.com by ggr...@gmail.com on 9 Sep 2011 at 12:30