Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
Created November 7, 2018 14:51
Embed
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
Foo.idr:10:11-34:
|
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