Typeclass implicit magic?

Syntax.idr

module Syntax
 
%default total

namespace SR
  public export
  interface Semiring a where
    constructor MkSemiring
    ---------------------------- OPERATIONS ------------------------------------
    -- A semiring (R) has two binary operations:
    (+) : a -> a -> a
    (*) : a -> a -> a
    -- And two identity elements, one for each operation:
    zero : a
    one : a
    --------------------------------LAWS ---------------------------------------
    -- Identity Laws for the additive identity:
    zeroLeftId : {x : a} -> zero + x = x
    zeroRightId : {x : a} -> x + zero = x
    -- Identity Laws for the multiplicative identity:
    oneLeftId : {x : a} -> one * x = x
    oneRightId : {x : a} -> x * one = x
    -- Plus must be commutative:
    plusCommutes : {x, y, z : a} -> (x + y) + z = x + (y + x)
    -- Multiplication is distributative:
    multLeftDistributes : {x, y, z : a} -> x * (y + z) = (x * y) + (x * z)
    multRightDistributes : {x, y , z : a} -> (x + y) * z = (x * z) + (y * z)
    -- Zero annihilates for multiplication:
    multZeroLeft : {x : a} -> zero * x = zero
    multZeroRight : {x : a} -> x * zero = zero

--------------- Forward Declarations of Mutual Types -------------------------

data Context : Type where

data TypeIn : Context -> Type where

data Term : (Semiring a) => a -> TypeIn gamma -> Type

namespace CtxScalar
  -- Scalar multiplication of semirings in contexts.
  public export
  (*) : (Semiring a) => a -> Context -> Context
  
------------------------- Mutual Definitions ---------------------------------

-- A context is a snoc list that is either empty...
-- Or snocs a semiring element and a type onto an existing context.
public export
data Context : Type where
  Empty : Context
  Extend : (Semiring r) => (gamma : Context)
        -> (r, TypeIn (SR.zero {a=r} * gamma)) -> Context

namespace CtxScalar
  -- (*) : (Semiring a) => a -> Context -> Context
  (*) k Empty = Empty
  (*) {a} k (Extend {r} xs (pi, ty)) = Extend {r=a} (k * xs) (SR.(*) k ?pihole , ?tyhole)