Skip to content

Instantly share code, notes, and snippets.

Created November 7, 2018 14:51
What would you like to do?
Why doesn't this typecheck?
module Foo
%default total
interface C a where
T' : Type
T : (a : Type) -> C a => Type
T a = T' {a}
interface (C a, Show (T a)) => D a where
p : (x : T a) -> (show x = show x)
Type checking ./Foo.idr
10 | interface (C a, Show (T a)) => D a where
| ~~~~~~~~~~~~~~~~~~~~~~~~
When checking type of Foo.p:
When checking argument x to type constructor =:
Can't find implementation for Show (T a)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment