История изменений

Исправление quasimoto, 31.01.13 21:16 (текущая версия) :

это лишь ограничение GHC, а на самом деле никаких логических противоречий в наличии такой возможности нет, верно ?

Ну, если написать

IntegralInstance :
  {A : Set} {n : ℕ} ⦃ multipable-iface : Multipable n ⦄ ⦃ integral-iface : Integral A ⦄
  → Multiple n A ≤ A
IntegralInstance {n = n} ⦃ multipable-iface = mi ⦄ ⦃ integral-iface = if ⦄ = record
  { sup = {!!}
  ; sub = {!!}
  }

RealFracInstance :
  {A : Set} {n : ℕ} ⦃ multipable-iface : Multipable n ⦄ ⦃ realfrac-iface : RealFrac A ⦄
  → Multiple n A ≤ A
RealFracInstance {n = n} ⦃ multipable-iface = mi ⦄ ⦃ realfrac-iface = rfi ⦄ = record
  { sup = {!!}
  ; sub = {!!}
  }

то при использовании, например, Multiple 2 Int ≤ Int можно найти в контексте A ~ Int, n ~ 2, Multiple 2 Int ≤ Int, Multipable 2 и Integral Int и не найти того же для RealFracInstance - всё получается хорошо. Агда сейчас так не умеет, точнее, она делает именно так, но плоско, то есть для простых инстансов - я могу написать в глобальный контекст int-is-num : Num Int и оно будет неявно подбираться, потом написать int-is-num-again : Num Int и будет ошибка, так что нужно явно указать какой инстанс я хочу (и тут ошибок уже не будет - может существовать сколько угодно перекрывающихся инстансов если они используются явно, конфликты нужно разрешать при неявном использовании). Если сделать более глубокий поиск - твой пример будет работать до тех пор пока точно так же можно найти в контексте однозначный (уникальный) набор «инстансов».

Исходная версия quasimoto, 31.01.13 21:07:

это лишь ограничение GHC, а на самом деле никаких логических противоречий в наличии такой возможности нет, верно ?

Ну, если написать

IntegralInstance :
  {A : Set} {n : ℕ} ⦃ multipable-iface : Multipable n ⦄ ⦃ integral-iface : Integral A ⦄
  → Multiple n A ≤ A
IntegralInstance {n = n} ⦃ multipable-iface = mi ⦄ ⦃ integral-iface = if ⦄ = record
  { sup = {!!}
  ; sub = {!!}
  }

RealFracInstance :
  {A : Set} {n : ℕ} ⦃ multipable-iface : Multipable n ⦄ ⦃ realfrac-iface : Integral A ⦄
  → Multiple n A ≤ A
RealFracInstance {n = n} ⦃ multipable-iface = mi ⦄ ⦃ realfrac-iface = rfi ⦄ = record
  { sup = {!!}
  ; sub = {!!}
  }