IndexedTypes.idr

module IndexedTypes

data Foo i = MkFoo
data FooInt i = MkFooInt Integer

mkFooInt : Foo i -> Integer -> FooInt i
mkFooInt _ = MkFooInt

addFoos : Foo i -> FooInt i -> FooInt i -> FooInt i
addFoos f (MkFooInt x) (MkFooInt y) = mkFooInt f (x + y)

-- Does not compile
bad : {i : Type} -> {j : Type} -> FooInt i
bad = let foo1 : Foo i = MkFoo
          foo2 : Foo j = MkFoo
          int1 = mkFooInt foo1 3
          int2 = mkFooInt foo2 4 in
          addFoos foo1 int1 int2

-- Compile
good : {i : Type} -> FooInt i
good = let foo1 : Foo i = MkFoo
           foo2 : Foo i = MkFoo
           int1 = mkFooInt foo1 3
           int2 = mkFooInt foo2 4 in
           addFoos foo1 int1 int2