{"action":"created","issue":{"url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/7","labels_url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/7/comments","events_url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/7/events","html_url":"https://github.com/Beluga-lang/Beluga/issues/7","id":81481766,"number":7,"title":"Identitiy substitutions in blocks (new syntax)","user":{"login":"pientka","id":5287544,"avatar_url":"https://avatars.githubusercontent.com/u/5287544?v=3","gravatar_id":"","url":"https://api.github.com/users/pientka","html_url":"https://github.com/pientka","followers_url":"https://api.github.com/users/pientka/followers","following_url":"https://api.github.com/users/pientka/following{/other_user}","gists_url":"https://api.github.com/users/pientka/gists{/gist_id}","starred_url":"https://api.github.com/users/pientka/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pientka/subscriptions","organizations_url":"https://api.github.com/users/pientka/orgs","repos_url":"https://api.github.com/users/pientka/repos","events_url":"https://api.github.com/users/pientka/events{/privacy}","received_events_url":"https://api.github.com/users/pientka/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"ajcave","id":790921,"avatar_url":"https://avatars.githubusercontent.com/u/790921?v=3","gravatar_id":"","url":"https://api.github.com/users/ajcave","html_url":"https://github.com/ajcave","followers_url":"https://api.github.com/users/ajcave/followers","following_url":"https://api.github.com/users/ajcave/following{/other_user}","gists_url":"https://api.github.com/users/ajcave/gists{/gist_id}","starred_url":"https://api.github.com/users/ajcave/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ajcave/subscriptions","organizations_url":"https://api.github.com/users/ajcave/orgs","repos_url":"https://api.github.com/users/ajcave/repos","events_url":"https://api.github.com/users/ajcave/events{/privacy}","received_events_url":"https://api.github.com/users/ajcave/received_events","type":"User","site_admin":false},"milestone":null,"comments":4,"created_at":"2015-05-27T14:57:36Z","updated_at":"2015-05-27T23:47:54Z","closed_at":null,"body":"This is an issue with the new syntax where we omit writing identity substitutions. \r\n\r\nFor example, the following works:\r\n \r\ntm: type.\r\ntp: type. \r\noft: tm -> tp -> type.\r\nschema xtG = some [t:tp] block (x:tm, u:oft x t);\r\n\r\ninductive Rxrt: {h:xtG} prop =\r\n| Rxrt_nil : Rxrt []\r\n| Rxrt_cons: Rxrt  [h] ->\r\n     Rxrt [h, b:block(x:tm, v:oft x A[..])];\r\n\r\nIn this case it solves the unification problem: A[ ^1] =?= ?Y[ ^1 ] during schema checking\r\n\r\nHowever, writing \r\n\r\ninductive Rxrt: {h:xtG} prop =\r\n| Rxrt_nil : Rxrt []\r\n| Rxrt_cons: Rxrt  [h] ->\r\n     Rxrt [h, b:block(x:tm, v:oft x A)];\r\n\r\ndoes not work, since it tries to solve the unification problem: A[ ^0 ] =?= ?Y[ ^1 ].\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/comments/106112443","html_url":"https://github.com/Beluga-lang/Beluga/issues/7#issuecomment-106112443","issue_url":"https://api.github.com/repos/Beluga-lang/Beluga/issues/7","id":106112443,"user":{"login":"pientka","id":5287544,"avatar_url":"https://avatars.githubusercontent.com/u/5287544?v=3","gravatar_id":"","url":"https://api.github.com/users/pientka","html_url":"https://github.com/pientka","followers_url":"https://api.github.com/users/pientka/followers","following_url":"https://api.github.com/users/pientka/following{/other_user}","gists_url":"https://api.github.com/users/pientka/gists{/gist_id}","starred_url":"https://api.github.com/users/pientka/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pientka/subscriptions","organizations_url":"https://api.github.com/users/pientka/orgs","repos_url":"https://api.github.com/users/pientka/repos","events_url":"https://api.github.com/users/pientka/events{/privacy}","received_events_url":"https://api.github.com/users/pientka/received_events","type":"User","site_admin":false},"created_at":"2015-05-27T23:47:54Z","updated_at":"2015-05-27T23:47:54Z","body":"Are you saying that \r\n\r\ninductive Rxrt: {h:xtG} prop =\r\n| Rxrt_nil : Rxrt []\r\n| Rxrt_cons: Rxrt [h] ->\r\nRxrt [h, b:block(x:tm, v:oft x A)];\r\n\r\nis equivalent to \r\n\r\ninductive Rxrt: {h:xtG} prop =\r\n| Rxrt_nil : Rxrt []\r\n| Rxrt_cons: Rxrt [h] ->\r\nRxrt [h, b:block(x:tm, v:oft x A[.., x])];\r\n\r\nand not \r\n\r\ninductive Rxrt: {h:xtG} prop =\r\n| Rxrt_nil : Rxrt []\r\n| Rxrt_cons: Rxrt [h] ->\r\nRxrt [h, b:block(x:tm, v:oft x A[..])];\r\n\r\n?\r\n\r\nIf this is the case, then I agree  that this is not a bug, but we should not give \r\n\r\nType block (x:tm, v:oft x (A ..)) doesn't check against schema .\r\n\r\nas an error, but \r\n\r\n Type block (x:tm, v:oft x A[ .., x]) doesn't check against schema .\r\n\r\n\r\n"}}