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

[Carter Schonwald]

the fine folks on IRC helped me get to the bottom of this, needed to remove
a needless level suc and replace a use of mkPair with Pair

On Thu, Feb 1, 2018 at 5:13 PM, Carter Schonwald <carter.schonwald at gmail.com
> wrote:

> 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/ed961ac0/attachment.html>