{"action":"opened","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1875","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1875/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1875/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1875/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/1875","id":55725984,"number":1875,"title":"Strange error messages in Sigma equality proofs","user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-01-28T08:09:39Z","updated_at":"2015-01-28T08:09:39Z","closed_at":null,"body":"The program\r\n````\r\n> cong2 : (f : a -> b -> c) -> (a1 = a2) -> (b1 = b2) -> f a1 b1 = f a2 b2\r\n> cong2 f Refl Refl = Refl\r\n\r\n> postulate lala : (b : Nat) -> (i : Nat) -> (j : Nat) ->\r\n>                  (p : LT i b) -> (q : LT j b) -> i = j -> p = q\r\n\r\n> P : Nat -> Type\r\n> P n = LT n 5\r\n\r\n> T : Type\r\n> T = Sigma Nat P\r\n\r\n> i : Nat\r\n> i = Z\r\n\r\n> j : Nat\r\n> j = Z\r\n\r\n> p : P i\r\n> q : P j\r\n\r\n> m : T\r\n> m = (i ** p)\r\n\r\n> n : T\r\n> n = (j ** q)\r\n\r\n> peq : p = q\r\n> peq = lala 5 i j p q Refl\r\n\r\n> r : m = n\r\n> r = cong2 MkSigma Refl peq\r\n```\r\nfails to type check with the error message\r\n````\r\n     When elaborating right hand side of r:\r\n     When elaborating an application of function Main.cong2:\r\n             Can't unify\r\n                     (=) {A = P i}\r\n                         {B = P i}\r\n                         p\r\n                         q\r\n             with\r\n                     (=) {A = (\\__pi_arg => P _) x}\r\n                         {B = (\\__pi_arg => P _) x}\r\n                         p\r\n                         q\r\n             \r\n             Specifically:\r\n                     Can't unify\r\n                             0\r\n                     with\r\n                             x\r\n```\r\nA simplified version:\r\n````\r\n> cong2 : (f : a -> b -> c) -> (a1 = a2) -> (b1 = b2) -> f a1 b1 = f a2 b2\r\n> cong2 f Refl Refl = Refl\r\n\r\n> P : Nat -> Type\r\n> P n = LT n 5\r\n\r\n> T : Type\r\n> T = Sigma Nat P\r\n\r\n> p : P Z\r\n> p = LTESucc LTEZero\r\n\r\n> m : T\r\n> m = (Z ** p)\r\n\r\n> n : T\r\n> n = (Z ** p)\r\n\r\n> q : m = n\r\n> q = cong2 MkSigma Refl Refl\r\n```\r\nalso fails with a rather strange error message:\r\n````\r\n     No such variable x\r\n```\r\nAny idea what is going on here ?\r\n\r\n\r\n\r\n"}}