<div dir="ltr">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</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 1, 2018 at 5:13 PM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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, <div><br></div><div>feedback would be appreciated, </div><div><a href="https://gist.github.com/cartazio/373eaa1ab726b2f6e651777a44b3f2b1" target="_blank">https://gist.github.com/<wbr>cartazio/<wbr>373eaa1ab726b2f6e651777a44b3f2<wbr>b1</a> <br></div><div>is the current version of the code</div><div><br></div><div>many thanks!</div><div>-Carter</div><div>also including it inline below </div><div><br></div><div><div>module auth where</div><div><br></div><div>open import Data.String</div><div>open import Data.Nat</div><div>open import Level</div><div>open import Data.Product</div><div>open import  Relation.Binary.<wbr>PropositionalEquality</div><div>open import Relation.Binary.<wbr>HeterogeneousEquality as Het</div><div><br></div><div><br></div><div>-- SignedBy will be a magic built in type that requires type checker support</div><div>-- seems likely in practice that i'll need to have some singleton structures</div><div>record SignedBy {ℓ } (t : Set ℓ  ) ( identity : String )  : Set ℓ  where</div><div>  field</div><div>    val : t</div><div>    uniqueCounter : ℕ --- unique natural number th</div><div>    hashOfVal : ℕ   --- nat number thats a Cryptographically Strong Hash of the canonical serialization of val</div><div>    signature  : String --- signature of concatenation of</div><div>                       ---(hashfOfVal , uniqueCounter), using the public key denotated by identity</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div>data AsDelegate : Set where</div><div>     IsDelegate : AsDelegate</div><div>     IsLeaf : AsDelegate</div><div>open AsDelegate</div><div><br></div><div><br></div><div>record TypeSing {ℓ : Level} ( tau : Set ℓ ) (v : tau) : Set ℓ  where</div><div>       field</div><div>         singVal : tau</div><div>         singIsSing : singVal ≡ v</div><div><br></div><div><br></div><div>record Pair {tx ty : Level} ( x : Set tx ) (y : Set ty ) : Set ( Level.suc (tx Level.⊔ ty )) where</div><div>  constructor mkPair</div><div>  field</div><div>    one : x</div><div>    two : y</div><div><br></div><div>data OnBehalfOf : String -> String -> AsDelegate -> Set  where</div><div>  Self : { x : String } ->  OnBehalfOf x x IsDelegate</div><div>  DelegatedTo : {root mid : String} -> (end : String)-></div><div>               SignedBy  ( mkPair (OnBehalfOf mid root IsDelegate)  (   TypeSing String end)) mid  -></div><div>               ---- not sure how to hack around this type universe issue... am I getting impredicative or wishing i was?</div><div>               OnBehalfOf end root IsDelegate</div><div>  LeafAuth : {root mid : String} -> (end : String) -> OnBehalfOf mid root IsDelegate -> OnBehalfOf end root IsLeaf</div><div><br></div><div>{-</div><div>equivalent datalog would be (roughly)</div><div>onBehalfOf(me,me,Delegate).</div><div>onBehalfOf(agent,<wbr>originalPerson,Delegate) :- onBehalfOf(mid,originalPerson,<wbr>Delegate),AddsDelegateFor(mid,<wbr>originalperson,agent)</div><div>onBhealfOf(leafAgent,<wbr>originalPerson,LEAF) :- onBehalfOf(mid,originalPerson,<wbr>Delegate),AddsLeafFor(mid,<wbr>originalperson,leafAgent)</div><div>-}</div></div><div><br></div></div>
</blockquote></div><br></div>