{"action":"opened","issue":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/229","labels_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/229/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/229/comments","events_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/229/events","html_url":"https://github.com/GaloisInc/cryptol/issues/229","id":84269090,"number":229,"title":"Cryptol infers types with extraneous type variables","user":{"login":"TomMD","id":137806,"avatar_url":"https://avatars.githubusercontent.com/u/137806?v=3","gravatar_id":"","url":"https://api.github.com/users/TomMD","html_url":"https://github.com/TomMD","followers_url":"https://api.github.com/users/TomMD/followers","following_url":"https://api.github.com/users/TomMD/following{/other_user}","gists_url":"https://api.github.com/users/TomMD/gists{/gist_id}","starred_url":"https://api.github.com/users/TomMD/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TomMD/subscriptions","organizations_url":"https://api.github.com/users/TomMD/orgs","repos_url":"https://api.github.com/users/TomMD/repos","events_url":"https://api.github.com/users/TomMD/events{/privacy}","received_events_url":"https://api.github.com/users/TomMD/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-06-02T23:52:38Z","updated_at":"2015-06-02T23:52:38Z","closed_at":null,"body":"In saw I noticed type variables were causing bitblast to fail.  It turns out that Cryptol is giving us some really ugly types:\r\n\r\nFor poly1305:\r\n\r\n```\r\nPoly1305> :type Poly1305\r\nPoly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m / 16,\r\n                                  rem == m - floorBlocks * 16) => [256] -> [m][8] -> [16][8]\r\n```\r\n\r\nOk, that one is fine. But when we apply it...\r\n\r\n```\r\nPoly1305> :type \\msg key -> Poly1305 (join (key :[32][8])) (msg : [256][8])\r\n\\msg key -> Poly1305 (join (key : [32][8]))\r\n                     (msg : [256][8]) : {a} [256][8] -> [32][8] -> [16][8]\r\n```\r\n\r\nWhat?  Where did `{a}` come from?"}}