The impossible happened

[agda]

The impossible happened

[GoogleCodeExporter]

The following error is probably related:

  module Bug where

  record AR : Set1 where
    field
      a : Set
      x : a

  module M (A : AR) where

    record MR : Set1 where
      field F : AR.a A -> Set

  record BR (A : AR) (AF : M.MR A) : Set1 where
    open AR A
    open M A
    open MR AF

    field f : F x

The code above type checks, but not if the field f is changed
slightly:

    field f : {B : Set} -> F x

  Bug.agda:18,26-27
  Set != (x' : _30 A AF) -> _31 A AF x' of type Set1
  when checking that x are valid arguments to a function of type Set

This seems to be related to issue 34, by the way.

Original comment by nils.anders.danielsson on 11 Dec 2007 at 4:09

[GoogleCodeExporter]

Original comment by [email protected] on 3 Jun 2008 at 8:31

• Changed state: Fixed