Idris dependent records with interface constraint on Type Constructor parameter

user_4071245 0
Viewed 395

Is it possible to have interface constraints on a parameter to a type constructor of a dependent record in idris? Say I have an interface Show : Type -> Type. Now I need to place a constraint on the following dependent record:

record Source s where
   constructor MkSource
   initial : s

I need to place a constraint on the parameter sso that it should always be a instance of Show. How to achieve this?

idris type-constraints
1 Answers

Idris is under heavy development but according to this recent email to the idris group the record syntax does currently not support constraining types with an interface:

https://groups.google.com/forum/#!topic/idris-lang/HMeTylslyFc

You will need to use data type syntax instead, e.g. 

module Main

data Source: Type -> Type where
    MkSource: Show s => s -> Source s


x: Source Int
x = MkSource 3

showSource: Source s -> String
showSource  (MkSource x) = show $ x

testMe: (showSource $ Main.x = "3")
testMe = Refl
user_10407850
Related