nested implicits

calling.idr

module Main
import Data.Maybe
import Decidable.Equality
import Data.Vect


hogefuga : {foo : {len : Nat} -> String -> Vect len String} -> Vect 2 String
hogefuga {foo} = foo {len=2} "foobar"

motif : {len : Nat} -> String -> Vect len String
motif {len} str = replicate len str

rap : Vect 2 String
rap = hogefuga {foo=motif}

infer.idr

module Main
import Data.Maybe
import Decidable.Equality
import Data.Vect


hogefuga : {foo : {a:Type} -> Show a => {len : Nat} -> a -> Vect len String} -> Vect 2 String
hogefuga {foo} = foo (the (List String) ["foobar"])

motif : Show a => {len : Nat} -> a -> Vect len String
motif {len} str = replicate len (show str)

rap : Vect 2 String
rap = hogefuga {foo=motif}

nested.idr

module Main
import Data.Maybe
import Decidable.Equality
import Data.Vect


hogefuga : {foo : {len : Nat} -> String -> Vect len String} -> Vect 2 String
hogefuga {foo} = foo {len=2} "foobar"

tc.idr

hogefuga : {foo : {a:Type} -> Show a => {len : Nat} -> a -> Vect len String} -> Vect 2 String
hogefuga {foo} = foo {a=List String} {len=2} ["foobar"]

motif : Show a => {len : Nat} -> a -> Vect len String
motif {len} str = replicate len (show str)

rap : Vect 2 String
rap = hogefuga {foo=motif}