[Agda] am I doing something fundamentally impredicative in this code? or is there a better approach

[Carter Schonwald]

Hello everyone! i'm messing around with trying to mock / model out first
class "signed values", and with a toy development  i'm getting some type
universe issues which makes me suspect i'm modelling it wrong,

feedback would be appreciated,
https://gist.github.com/cartazio/373eaa1ab726b2f6e651777a44b3f2b1
is the current version of the code

many thanks!
-Carter
also including it inline below

module auth where

open import Data.String
open import Data.Nat
open import Level
open import Data.Product
open import  Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as Het


-- SignedBy will be a magic built in type that requires type checker support
-- seems likely in practice that i'll need to have some singleton structures
record SignedBy {ℓ } (t : Set ℓ  ) ( identity : String )  : Set ℓ  where
  field
    val : t
    uniqueCounter : ℕ --- unique natural number th
    hashOfVal : ℕ   --- nat number thats a Cryptographically Strong Hash of
the canonical serialization of val
    signature  : String --- signature of concatenation of
                       ---(hashfOfVal , uniqueCounter), using the public
key denotated by identity





data AsDelegate : Set where
     IsDelegate : AsDelegate
     IsLeaf : AsDelegate
open AsDelegate


record TypeSing {ℓ : Level} ( tau : Set ℓ ) (v : tau) : Set ℓ  where
       field
         singVal : tau
         singIsSing : singVal ≡ v


record Pair {tx ty : Level} ( x : Set tx ) (y : Set ty ) : Set ( Level.suc
(tx Level.⊔ ty )) where
  constructor mkPair
  field
    one : x
    two : y

data OnBehalfOf : String -> String -> AsDelegate -> Set  where
  Self : { x : String } ->  OnBehalfOf x x IsDelegate
  DelegatedTo : {root mid : String} -> (end : String)->
               SignedBy  ( mkPair (OnBehalfOf mid root IsDelegate)  (
 TypeSing String end)) mid  ->
               ---- not sure how to hack around this type universe issue...
am I getting impredicative or wishing i was?
               OnBehalfOf end root IsDelegate
  LeafAuth : {root mid : String} -> (end : String) -> OnBehalfOf mid root
IsDelegate -> OnBehalfOf end root IsLeaf

{-
equivalent datalog would be (roughly)
onBehalfOf(me,me,Delegate).
onBehalfOf(agent,originalPerson,Delegate) :-
onBehalfOf(mid,originalPerson,Delegate),AddsDelegateFor(mid,originalperson,agent)
onBhealfOf(leafAgent,originalPerson,LEAF) :-
onBehalfOf(mid,originalPerson,Delegate),AddsLeafFor(mid,originalperson,leafAgent)
-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180201/5f589fbd/attachment.html>