So a straightforward translation of extensible-effects gives universe errors..
-
-
Replying to @dannygratzer
@jozefg28 difficulty with universe polymorphism? how improbable! /s
1 reply 0 retweets 0 likes -
Replying to @beka_valentine
@psygnisfive I know right :) Looks like the actual problem is predicativity though :/1 reply 0 retweets 0 likes -
Replying to @dannygratzer
@jozefg28 im sure the idris people have a reasonable response /cc
@edwinbrady1 reply 0 retweets 0 likes
Replying to @beka_valentine
@psygnisfive @jozefg28 If it’s universe errors in idris, I’m relieved that the universe checking actually does something sometimes :).
2:29 AM - 21 Jul 2014
0 replies
0 retweets
1 like
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.