[Agda] example with --sharing

[Sergei Meshveliani]

I fail to link to "Report a bug", so I report here.

This program is not type-checked by

             agda $agdaLibOpts --sharing Foo.agda

(in Development Agda of September16, 2016):

----------------------------------------------------------------------
open import Relation.Binary  using (Setoid)
open import Data.Maybe as Mb using (Maybe; just; nothing; Eq)

module _ {α α=} {A : Setoid α α=}
  where
  open Setoid A using (_≈_) renaming (Carrier to C; refl to ≈refl)
  open Setoid (Mb.setoid A) renaming (Carrier to C'; _≈_ to _='_)

  fromMb : C → Maybe C → C
  fromMb _ (just x) =  x
  fromMb n nothing  =  n

  cong-fromMb : {n n' : C} → {m m' : C'} → n ≈ n' → m =' m' →
                                              fromMb n m ≈ fromMb n' m'

  cong-fromMb {n} {n'} {m} {m'} n=n' m=m'  with  m | m' | m=m'
  ...
      | just _  | just _  | Mb.Eq.just x=y =  x=y
  ... | nothing | nothing | _              =  n=n'
  ... | nothing | just _  | ()
------------------------------------------------------------------------


Regards,

------
Sergei