New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Regression in unifier, possibly related to modules and/or heterogeneous constraints #1071

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 3 comments

Comments

Projects
None yet
2 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

-- The code below is accepted by Agda 2.3.2.

module Bug where

postulate
  F : Set → Set

module M (_ : Set₁) where
  postulate A : Set

open M Set

data P : Set → Set₁ where
  c : (R : Set) → P (F R)

data Q : (R : Set) → R → P R → Set₁ where
  d : (R : Set) (f : F R) → Q (F R) f (c R)

Foo : (f : F A) → Q (F A) f (c A) → Set₁
Foo ._ (d ._ _) = Set

-- Bug.agda:20,9-15
-- Refuse to solve heterogeneous constraint f₁ : F A =?= f : F A
-- when checking that the pattern d ._ _ has type Q (F A) f (c A)

Original issue reported on code.google.com by nils.anders.danielsson on 28 Feb 2014 at 8:00

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

    unifyAtomHH aHH0 u v tryAgain = do
      let (aHH, homogeneous, a) = case aHH0 of
            Hom a                -> (aHH0, True, a)
            Het a1 a2 | a1 == a2 -> (Hom a1, True, a1) -- BRITTLE: just checking syn.eq.

As the code says, checking for homogeneous case is brittle. ;-)  You broke it 
now!
Maybe this regression is related to changed normalization strategy?

Original comment by andreas....@gmail.com on 2 Mar 2014 at 9:37

  • Added labels: Unify
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

We get

unifyHH (f) =?= (f') : F R || F A
unifyHH (reduced) (f) =?= (f') : F A || F A
unifyAtom f =?= f' (flexible) : F A || F A
aHH = Het 
(El {getSort = Type (Max []), unEl = Def Issue1071.F [Apply []r(Def 
Issue1071.M.A [Apply []r(Sort (Type (Max [])))])]}) 
(El {getSort = Type (Max []), unEl = Def Issue1071.F [Apply []r(Def 
Issue1071._.A [])]})

Internally F A is different to F A since one is M.A Set and the other is _.A.

Original comment by andreas....@gmail.com on 2 Mar 2014 at 10:27

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Mon Mar  3 10:19:40 CET 2014  Andreas Abel <andreas.abel@ifi.lmu.de>
  * Fixed issue 1071.  Failing heterogeneous unification problems are now rechecked a third time if can be made homogeneous by checking type equality.


Original comment by andreas....@gmail.com on 3 Mar 2014 at 9:33

  • Changed title: Regression in unifier, possibly related to modules and/or heterogeneous constraints
  • Changed state: Fixed

@asr asr modified the milestone: 2.3.4 Aug 16, 2015

@asr asr added the unification label Jan 13, 2016

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment