Broken attempt to embed a DSL for operations on 3D regular grids with bounds checking into Idris

nebo.idr

module Main

import Data.Vect
import Data.Fin

data NumType =
  NAT
  | FIN Nat

data LocType =
  Vol
  | XFace
  | YFace
  | ZFace
  | Any

data ScalarType =
  DOUBLE
  | INT

data DataType =
  DataTypeC NumType NumType NumType ScalarType

interpNumType : NumType -> Type
interpNumType NAT = Nat
interpNumType (FIN n) = Fin n

interpScalarType : ScalarType -> Type
interpScalarType DOUBLE = Double
interpScalarType INT = Int

interpDataType : DataType -> Type
interpDataType (DataTypeC x y z s) =
  (interpNumType x) -> (interpNumType y) -> (interpNumType z) -> (interpScalarType s)

data NeboExpr : (t : DataType) -> (l : LocType) -> Type where
  NeboExprC : (interpDataType t) -> NeboExpr t l

neboField : {x : Nat} -> {y : Nat} -> {z : Nat} -> (t : ScalarType) -> (l : LocType) ->
            Vect z (Vect y (Vect x (interpScalarType t))) ->
            (NeboExpr (DataTypeC (FIN x) (FIN y) (FIN z) t) l)
neboField {x} {y} {z} t l arr =
  (NeboExprC
    (\x, y, z => index x (index y (index z arr))))

neboConst : (t : ScalarType) -> (interpScalarType t) -> (NeboExpr (DataTypeC NAT NAT NAT t) Any)
neboConst t n = (NeboExprC (\x, y, z => n))

data MeetNumType : (t1 : NumType) -> (t2 : NumType) -> (t3 : NumType) -> Type where
  MNTC1 : (a : NumType) -> MeetNumType NAT a   a
  MNTC2 : (a : NumType) -> MeetNumType a   NAT a
  MNTC3 : (a : NumType) -> MeetNumType a   a   a

data MeetLocType : LocType -> LocType -> LocType -> Type where
  MLTC1 : (a : LocType) -> MeetLocType Any a   a
  MLTC2 : (a : LocType) -> MeetLocType a   Any a
  MLTC3 : (a : LocType) -> MeetLocType a   a   a

data MeetDataType : DataType -> DataType -> DataType -> Type where
  MDTC1 : ({auto p1 : MeetNumType x1 x2 x3} ->
          {auto p2 : MeetNumType y1 y2 y3} ->
          {auto p3 : MeetNumType z1 z2 z3} ->
          (MeetDataType (DataTypeC x1 y1 z1 s) (DataTypeC x2 y2 z2 s) (DataTypeC x3 y3 z3 s)))

neboAdd : {auto p1 : MeetDataType d1 d2 d3} ->
          {auto p2 : MeetLocType  l1 l2 l3} ->
          NeboExpr d1 l1 -> NeboExpr d2 l2 -> NeboExpr d3 l3
neboAdd (NeboExprC e1) (NeboExprC e2) =
  (NeboExprC (\x, y, z => (e1 x y z) + (e2 x y z)))

--$ idris nebo.idr
     --____    __     _
    --/  _/___/ /____(_)____
    --/ // __  / ___/ / ___/     Version 0.9.18-
  --_/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 --/___/\__,_/_/  /_/____/       Type :? for help

--Idris is free software with ABSOLUTELY NO WARRANTY.
--For details type :warranty.
--Type checking ./nebo.idr
--nebo.idr:69:31:When elaborating right hand side of neboAdd:
--When elaborating an application of function Data.Fin.+:
        --e1 does not have a function type (interpDataType d1)
--Metavariables: Main.neboAdd
--*nebo>
--Bye bye

small.idr

module Main

import Data.Vect
import Data.Fin

data NumType =
  NAT
  | FIN Nat

data DataType =
  DataTypeC NumType

interpNumType : NumType -> Type
interpNumType NAT = Nat
interpNumType (FIN n) = Fin n

interpDataType : DataType -> Type
interpDataType (DataTypeC x) = (interpNumType x) -> Double

data NeboExpr : (t : DataType)  -> Type where
  NeboExprC : (interpDataType t) -> NeboExpr t

data MeetNumType : (t1 : NumType) -> (t2 : NumType) -> (t3 : NumType) -> Type where
  MNTC1 : (a : NumType) -> MeetNumType NAT a   a
  MNTC2 : (a : NumType) -> MeetNumType a   NAT a
  MNTC3 : (a : NumType) -> MeetNumType a   a   a

data MeetDataType : DataType -> DataType -> DataType -> Type where
  MDTC1 : ({auto p1 : MeetNumType x1 x2 x3} ->
          (MeetDataType (DataTypeC x1) (DataTypeC x2) (DataTypeC x3)))

neboAdd : {auto p1 : MeetDataType d1 d2 d3} ->
          NeboExpr d1 -> NeboExpr d2 -> NeboExpr d3
neboAdd (NeboExprC e1) (NeboExprC e2) =
  (NeboExprC (\x => (e1 x) + (e2 x)))

     --____    __     _
    --/  _/___/ /____(_)____
    --/ // __  / ___/ / ___/     Version 0.9.18-
  --_/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 --/___/\__,_/_/  /_/____/       Type :? for help

--Idris is free software with ABSOLUTELY NO WARRANTY.
--For details type :warranty.
--Type checking ./small.idr
--small.idr:34:9:When elaborating right hand side of neboAdd:
--When elaborating an application of function Data.Fin.+:
        --e1 does not have a function type (interpDataType d1)
--Metavariables: Main.neboAdd