{"action":"created","issue":{"url":"https://api.github.com/repos/goldfirere/singletons/issues/296","repository_url":"https://api.github.com/repos/goldfirere/singletons","labels_url":"https://api.github.com/repos/goldfirere/singletons/issues/296/labels{/name}","comments_url":"https://api.github.com/repos/goldfirere/singletons/issues/296/comments","events_url":"https://api.github.com/repos/goldfirere/singletons/issues/296/events","html_url":"https://github.com/goldfirere/singletons/issues/296","id":292531016,"number":296,"title":"Failure to single let-bound subexpression with a type signature","user":{"login":"RyanGlScott","id":2364661,"avatar_url":"https://avatars2.githubusercontent.com/u/2364661?v=4","gravatar_id":"","url":"https://api.github.com/users/RyanGlScott","html_url":"https://github.com/RyanGlScott","followers_url":"https://api.github.com/users/RyanGlScott/followers","following_url":"https://api.github.com/users/RyanGlScott/following{/other_user}","gists_url":"https://api.github.com/users/RyanGlScott/gists{/gist_id}","starred_url":"https://api.github.com/users/RyanGlScott/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RyanGlScott/subscriptions","organizations_url":"https://api.github.com/users/RyanGlScott/orgs","repos_url":"https://api.github.com/users/RyanGlScott/repos","events_url":"https://api.github.com/users/RyanGlScott/events{/privacy}","received_events_url":"https://api.github.com/users/RyanGlScott/received_events","type":"User","site_admin":false},"labels":[{"id":20376946,"url":"https://api.github.com/repos/goldfirere/singletons/labels/bug","name":"bug","color":"fc2929","default":true}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":11,"created_at":"2018-01-29T19:29:39Z","updated_at":"2018-02-06T15:55:16Z","closed_at":null,"author_association":"COLLABORATOR","body":"Originally observed in https://github.com/goldfirere/singletons/pull/295#discussion_r164288565. This program:\r\n\r\n```haskell\r\nimport Data.Kind\r\n\r\ndata MyProxy (a :: Type) = MyProxy\r\n\r\nf :: forall a. MyProxy a -> MyProxy a\r\nf MyProxy = \r\n  let x = let z :: MyProxy a\r\n              z = MyProxy in z\r\n  in x\r\n```\r\n\r\nWill correctly promote, but not correctly single, as this program demonstrates:\r\n\r\n```haskell\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Singletons.Prelude\r\nimport Data.Singletons.TH\r\n\r\n$(singletons [d|\r\n  data MyProxy (a :: Type) = MyProxy\r\n\r\n  f :: forall a. MyProxy a -> MyProxy a\r\n  f MyProxy =\r\n    let x = let z :: MyProxy a\r\n                z = MyProxy in z\r\n    in x\r\n  |])\r\n```\r\n```\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs -ddump-splices\r\n[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )\r\nBug.hs:(14,3)-(22,4): Splicing declarations\r\n    singletons\r\n      [d| f_a32l ::\r\n            forall a_a3vI. MyProxy_a32j a_a3vI -> MyProxy_a32j a_a3vI\r\n          f_a32l MyProxy_a32k\r\n            = let\r\n                x_a3vJ\r\n                  = let\r\n                      z_a3vK :: MyProxy_a32j a_a3vI\r\n                      z_a3vK = MyProxy_a32k\r\n                    in z_a3vK\r\n              in x_a3vJ\r\n          \r\n          data MyProxy_a32j (a_a3vH :: Type) = MyProxy_a32k |]\r\n  ======>\r\n    data MyProxy_a6jb (a_a6jd :: Type) = MyProxy_a6jc\r\n    f_a6ja :: forall a_a6j9. MyProxy_a6jb a_a6j9 -> MyProxy_a6jb a_a6j9\r\n    f_a6ja MyProxy_a6jc\r\n      = let\r\n          x_a6je\r\n            = let\r\n                z_a6jf :: MyProxy_a6jb a_a6j9\r\n                z_a6jf = MyProxy_a6jc\r\n              in z_a6jf\r\n        in x_a6je\r\n    type MyProxySym0 = MyProxy_a6jc\r\n    type Let6989586621679034055ZSym0 = Let6989586621679034055Z\r\n    type family Let6989586621679034055Z :: MyProxy_a6jb a_a6j9 where\r\n      Let6989586621679034055Z = MyProxySym0\r\n    type Let6989586621679034054XSym0 = Let6989586621679034054X\r\n    type family Let6989586621679034054X where\r\n      Let6989586621679034054X = Let6989586621679034055ZSym0\r\n    type FSym1 (t_a6jg :: MyProxy_a6jb a6989586621679034043) = F t_a6jg\r\n    instance SuppressUnusedWarnings FSym0 where\r\n      suppressUnusedWarnings\r\n        = snd ((GHC.Tuple.(,) FSym0KindInference) GHC.Tuple.())\r\n    data FSym0 (l_a6jh :: TyFun (MyProxy_a6jb a6989586621679034043) (MyProxy_a6jb a6989586621679034043))\r\n      = forall arg_a6ji. SameKind (Apply FSym0 arg_a6ji) (FSym1 arg_a6ji) =>\r\n        FSym0KindInference\r\n    type instance Apply FSym0 l_a6jh = F l_a6jh\r\n    type family F (a_a6jj :: MyProxy_a6jb a_a6j9) :: MyProxy_a6jb a_a6j9 where\r\n      F MyProxy_a6jc = Let6989586621679034054XSym0\r\n    sF ::\r\n      forall (t_a6jm :: MyProxy_a6jb a_a6j9).\r\n      Sing t_a6jm -> Sing (Apply FSym0 t_a6jm :: MyProxy_a6jb a_a6j9)\r\n    sF SMyProxy\r\n      = let\r\n          sX :: Sing Let6989586621679034054XSym0\r\n          sX\r\n            = let\r\n                sZ :: Sing (Let6989586621679034055ZSym0 :: MyProxy_a6jb a_a6j9)\r\n                sZ = SMyProxy\r\n              in sZ\r\n        in sX\r\n    data instance Sing (z_a6jn :: MyProxy_a6jb a_a6jd)\r\n      where SMyProxy :: Sing MyProxy_a6jc\r\n    type SMyProxy = (Sing :: MyProxy_a6jb a_a6jd -> Type)\r\n    instance SingKind a_a6jd => SingKind (MyProxy_a6jb a_a6jd) where\r\n      type Demote (MyProxy_a6jb a_a6jd) = MyProxy_a6jb (Demote a_a6jd)\r\n      fromSing SMyProxy = MyProxy_a6jc\r\n      toSing MyProxy_a6jc = SomeSing SMyProxy\r\n    instance SingI MyProxy_a6jc where\r\n      sing = SMyProxy\r\n\r\nBug.hs:14:3: error:\r\n    • Could not deduce: a ~ a1\r\n      from the context: t ~ 'MyProxy\r\n        bound by a pattern with constructor:\r\n                   SMyProxy :: forall a. Sing 'MyProxy,\r\n                 in an equation for ‘sF’\r\n        at Bug.hs:(14,3)-(22,4)\r\n      ‘a’ is a rigid type variable bound by\r\n        the type signature for:\r\n          sF :: forall a (t :: MyProxy a). Sing t -> Sing (Apply FSym0 t)\r\n        at Bug.hs:(14,3)-(22,4)\r\n      ‘a1’ is a rigid type variable bound by\r\n        the type signature for:\r\n          sX :: forall a1. Sing Let6989586621679034054XSym0\r\n        at Bug.hs:(14,3)-(22,4)\r\n      Expected type: Sing Let6989586621679034054XSym0\r\n        Actual type: Sing Let6989586621679034055ZSym0\r\n    • In the expression: sZ\r\n      In the expression:\r\n        let\r\n          sZ :: Sing (Let6989586621679034055ZSym0 :: MyProxy a_a6j9)\r\n          sZ = SMyProxy\r\n        in sZ\r\n      In an equation for ‘sX’:\r\n          sX\r\n            = let\r\n                sZ :: Sing (Let6989586621679034055ZSym0 :: MyProxy a_a6j9)\r\n                sZ = SMyProxy\r\n              in sZ\r\n    • Relevant bindings include\r\n        sZ :: Sing Let6989586621679034055ZSym0 (bound at Bug.hs:14:3)\r\n        sX :: Sing Let6989586621679034054XSym0 (bound at Bug.hs:14:3)\r\n        sF :: Sing t -> Sing (Apply FSym0 t) (bound at Bug.hs:14:3)\r\n   |\r\n14 | $(singletons [d|\r\n   |   ^^^^^^^^^^^^^^...\r\n```\r\n\r\nFrom the `-ddump-splices` output, we can see why:\r\n\r\n```haskell\r\n    sF ::\r\n      forall (t_a6jm :: MyProxy_a6jb a_a6j9).\r\n      Sing t_a6jm -> Sing (Apply FSym0 t_a6jm :: MyProxy_a6jb a_a6j9)\r\n    sF SMyProxy\r\n      = let\r\n          sX :: Sing Let6989586621679034054XSym0\r\n          sX\r\n            = let\r\n                sZ :: Sing (Let6989586621679034055ZSym0 :: MyProxy_a6jb a_a6j9)\r\n                sZ = SMyProxy\r\n              in sZ\r\n        in sX\r\n```\r\n\r\nGHC is unable to conclude that the `a1`—which is implicitly quantified in the type signature of `sX :: Sing Let6989586621679034054XSym0` —is the same `a` as in `sF`'s type signature.\r\n\r\nI would bet that we could fix this by making that `a1` argument to `Let6989586621679034054XSym0` visible and propagating that change through to its defunctionalization symbols, but I don't know how much effort that would entail."},"comment":{"url":"https://api.github.com/repos/goldfirere/singletons/issues/comments/363466900","html_url":"https://github.com/goldfirere/singletons/issues/296#issuecomment-363466900","issue_url":"https://api.github.com/repos/goldfirere/singletons/issues/296","id":363466900,"user":{"login":"RyanGlScott","id":2364661,"avatar_url":"https://avatars2.githubusercontent.com/u/2364661?v=4","gravatar_id":"","url":"https://api.github.com/users/RyanGlScott","html_url":"https://github.com/RyanGlScott","followers_url":"https://api.github.com/users/RyanGlScott/followers","following_url":"https://api.github.com/users/RyanGlScott/following{/other_user}","gists_url":"https://api.github.com/users/RyanGlScott/gists{/gist_id}","starred_url":"https://api.github.com/users/RyanGlScott/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RyanGlScott/subscriptions","organizations_url":"https://api.github.com/users/RyanGlScott/orgs","repos_url":"https://api.github.com/users/RyanGlScott/repos","events_url":"https://api.github.com/users/RyanGlScott/events{/privacy}","received_events_url":"https://api.github.com/users/RyanGlScott/received_events","type":"User","site_admin":false},"created_at":"2018-02-06T15:55:16Z","updated_at":"2018-02-06T15:55:16Z","author_association":"COLLABORATOR","body":"I don't think the `PartialTypeSignatures` approach would even fix the problem. For starters, if I use your suggested replacement for `sGo`'s type signature:\r\n\r\n```haskell\r\nsFoldr ::\r\n  forall (t_a6nE :: TyFun a_a6mQ (TyFun b_a6mR b_a6mR\r\n                                  -> Type)\r\n                    -> Type)\r\n         (t_a6nF :: b_a6mR)\r\n         (t_a6nG :: [a_a6mQ]).\r\n  Sing t_a6nE\r\n  -> Sing t_a6nF\r\n     -> Sing t_a6nG\r\n        -> Sing (Apply (Apply (Apply FoldrSym0 t_a6nE) t_a6nF) t_a6nG :: b_a6mR)\r\nsFoldr\r\n  (sK :: Sing k_a6nf)\r\n  (sZ :: Sing z_a6ng)\r\n  (sA_6989586621679034295 :: Sing a_6989586621679034295_a6nh)\r\n  = (applySing\r\n       (let\r\n          sGo :: _ -> Sing (Apply (Let6989586621679034300GoSym3 _ _ _) _)\r\n          sGo SNil = sZ\r\n          sGo\r\n            (SCons (sY :: Sing y_a6nC)\r\n                                                                      (sYs :: Sing ys_a6nD))\r\n            = (applySing ((applySing sK) sY))\r\n                ((applySing\r\n                    ((singFun1\r\n                        @(Let6989586621679034300GoSym3 k_a6nf z_a6ng a_6989586621679034295_a6nh))\r\n                       sGo))\r\n                   sYs)\r\n        in\r\n          (singFun1\r\n             @(Let6989586621679034300GoSym3 k_a6nf z_a6ng a_6989586621679034295_a6nh))\r\n            sGo))\r\n      sA_6989586621679034295\r\n```\r\n\r\nThen it'll fail in a different way:\r\n\r\n```\r\nBug.hs:99:11: error:\r\n    • Couldn't match type ‘Let6989586621679034300Go w0 w1 w2 w3’\r\n                     with ‘Let6989586621679034300Go w w4 w5 w6’\r\n      Expected type: Sing z -> Sing (Let6989586621679034300Go w w4 w5 w6)\r\n        Actual type: Sing z\r\n                     -> Sing (Let6989586621679034300Go w0 w1 w2 w3)\r\n      NB: ‘Let6989586621679034300Go’ is a type function, and may not be injective\r\n      The type variables ‘w0’, ‘w1’, ‘w2’, ‘w3’ are ambiguous\r\n    • In the ambiguity check for the inferred type for ‘sGo’\r\n      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n      When checking the inferred type\r\n        sGo :: forall k1 k2 a k3 (z :: [a]) (w1 :: k1\r\n                                                   ~> (k2\r\n                                                       ~> k2)) (w2 :: k2) (w3 :: k3) (w4 :: [k1]).\r\n               Sing z -> Sing (Let6989586621679034300Go w1 w2 w3 w4)\r\n      In the first argument of ‘applySing’, namely\r\n        ‘(let\r\n            sGo :: _ -> Sing (Apply (Let6989586621679034300GoSym3 _ _ _) _)\r\n            sGo SNil = sZ\r\n            sGo (SCons (sY :: Sing y_a6nC) (sYs :: Sing ys_a6nD))\r\n              = (applySing ((applySing sK) sY))\r\n                  ((applySing\r\n                      ((singFun1\r\n                          @(Let6989586621679034300GoSym3 k_a6nf z_a6ng a_6989586621679034295_a6nh))\r\n                         sGo))\r\n                     sYs)\r\n          in\r\n            (singFun1\r\n               @(Let6989586621679034300GoSym3 k_a6nf z_a6ng a_6989586621679034295_a6nh))\r\n              sGo)’\r\n   |\r\n99 |           sGo SNil = sZ\r\n   |           ^^^^^^^^^^^^^...\r\n```\r\n\r\nMoreover, this wouldn't even fix the [original program](https://github.com/goldfirere/singletons/issues/296#issue-292531016), would it? After all, the problematic type signature was:\r\n\r\n```\r\nsX :: Sing Let6989586621679034054XSym0\r\n```\r\n\r\nBut this has no arguments, so this wouldn't even be changed under the new scheme, leaving us in the same situation as before."}}
{"actor":{"display_login":"RyanGlScott"}}