[Agda] strange " ,′ "

[Andreas Abel]

The use of _,'_ for non-dependent pairs helps Agda to type check, when 
the dependent _,_ produces unsolvable constraints.

Unfortunately, such workarounds are sometimes needed, as higher-order 
unification is undecidable.

Note: I did not look at your specific example.  If you think it is a 
bug, please provide a /small/ test case.

Cheers,
Andreas

On 20.09.2014 17:47, Sergei Meshveliani wrote:
> People,
> for the code fragment
>
> ----------------------------------------
>     let ys = del _≟_ x xs'
>
>         ⊆to : x ∷ xs ⊆ x ∷ ys
>         ⊆to {z} z∈x:xs =
>             case
>                 (x ≟ z , z∈x:xs)
>              of \
>              { (_ ,       here z=x  ) → here z=x
>              ; (yes x=z , _         ) → here $ ≈sym x=z
>              ; (no x≉z ,  there z∈xs) →
>                                 let z∈xs' = proj₁ xs='xs' z∈xs
>                                     z∈ys  = ∈del-x-xs-if _≟_ x≉z z∈xs'
>                                 in  there z∈ys
>              }
>
>         ⊆from : x ∷ ys ⊆ x ∷ xs
>         ⊆from {z} z∈x:ys =
>               case
>                   (x ≟ z , z∈x:ys)
>               of \
>               { (_ ,       here z=x  ) → here z=x
>               ; (yes x=z , _         ) → here $ ≈sym x=z
>               ; (no x≉z ,  there z∈ys) → let z∈xs' : z ∈ xs'
>                                              z∈xs' = del-x-xs⊆xs _≟_ z∈ys
>                                              z∈xs = proj₂ xs='xs' z∈xs'
>                                          in  there z∈xs
>               }
>     ...
> -----------------------------------------
>
>
> Agda 2.4.2  reports
>
>    Cannot instantiate the metavariable _1653 to solution x₁ ∷ xs₁
>    ...
>
> This is for the line of the first pattern after the second  `of'
> -- not the first one!
> And this is fixed by replacing _,_ with _,′_ in the pair after the
> second  'case'.
>
> This all looks strange, because  ⊆to  and  ⊆from  are similar and
> symmetric
> (and it is difficult to guess of this _,′_).
>
> Is this a bug?
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/