[GHC] #12542: Unexpected failure.. (bug?)
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- From [http://www.cse.chalmers.se/~emax/documents/axelsson2012generic- slides.pdf A Generic Abstract Syntax Model for Embedded Languages]([http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf paper]) {{{#!hs infixr :-> infixl 1 :$ data Full a data a :-> b data AST dom sig where Sym :: dom sig -> AST dom sig (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig class Binding dom where viewVar :: dom a -> Maybe Integer viewBnd :: dom (a :-> b) -> Maybe Integer freeVars :: Binding dom => AST dom a -> [Integer] freeVars = \case Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined where (a, _) = (viewVar, undefined) (_, b) = (undefined, viewBnd) }}} and so does {{{#!hs where a = viewVar b = viewBnd }}} but {{{#!hs where (a, b) = (viewVar, viewBnd) }}} yields {{{ tSvp.hs:20:5-31: error: … • Could not deduce (Binding dom0) from the context: Binding dom bound by the type signature for: freeVars :: Binding dom => AST dom a -> [Integer] at /tmp/tSvp.hs:14:1-49 or from: Binding dom2 bound by the inferred type for ‘a’: Binding dom2 => dom2 a1 -> Maybe Integer at /tmp/tSvp.hs:20:5-31 The type variable ‘dom0’ is ambiguous • When checking that the inferred type a :: forall k k1 (dom :: * -> *) a (dom1 :: * -> *) (a1 :: k) (b :: k1). (Binding dom1, Binding dom) => dom a -> Maybe Integer is as general as its inferred signature a :: forall (dom :: * -> *) a. Binding dom => dom a -> Maybe Integer In an equation for ‘freeVars’: freeVars = \case { Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined } where (a, b) = (viewVar, viewBnd) tSvp.hs:20:5-31: error: … • Could not deduce (Binding dom1) from the context: Binding dom bound by the type signature for: freeVars :: Binding dom => AST dom a -> [Integer] at /tmp/tSvp.hs:14:1-49 or from: Binding dom2 bound by the inferred type for ‘b’: Binding dom2 => dom2 (a1 :-> b) -> Maybe Integer at /tmp/tSvp.hs:20:5-31 The type variable ‘dom1’ is ambiguous • When checking that the inferred type b :: forall k k1 (dom :: * -> *) a (dom1 :: * -> *) (a1 :: k) (b :: k1). (Binding dom1, Binding dom) => dom1 (a1 :-> b) -> Maybe Integer is as general as its inferred signature b :: forall k k1 (dom :: * -> *) (a :: k) (b :: k1). Binding dom => dom (a :-> b) -> Maybe Integer In an equation for ‘freeVars’: freeVars = \case { Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined } where (a, b) = (viewVar, viewBnd) Compilation failed. }}} Is this intentional? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -2,2 +2,2 @@ - slides.pdf A Generic Abstract Syntax Model for Embedded - Languages]([http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf + slides.pdf A Generic Abstract Syntax Model for Embedded Languages] + ([http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf @@ -30,1 +30,1 @@ - and so does + works, and so does New description: From [http://www.cse.chalmers.se/~emax/documents/axelsson2012generic- slides.pdf A Generic Abstract Syntax Model for Embedded Languages] ([http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf paper]) {{{#!hs infixr :-> infixl 1 :$ data Full a data a :-> b data AST dom sig where Sym :: dom sig -> AST dom sig (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig class Binding dom where viewVar :: dom a -> Maybe Integer viewBnd :: dom (a :-> b) -> Maybe Integer freeVars :: Binding dom => AST dom a -> [Integer] freeVars = \case Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined where (a, _) = (viewVar, undefined) (_, b) = (undefined, viewBnd) }}} works, and so does {{{#!hs where a = viewVar b = viewBnd }}} but {{{#!hs where (a, b) = (viewVar, viewBnd) }}} yields {{{ tSvp.hs:20:5-31: error: … • Could not deduce (Binding dom0) from the context: Binding dom bound by the type signature for: freeVars :: Binding dom => AST dom a -> [Integer] at /tmp/tSvp.hs:14:1-49 or from: Binding dom2 bound by the inferred type for ‘a’: Binding dom2 => dom2 a1 -> Maybe Integer at /tmp/tSvp.hs:20:5-31 The type variable ‘dom0’ is ambiguous • When checking that the inferred type a :: forall k k1 (dom :: * -> *) a (dom1 :: * -> *) (a1 :: k) (b :: k1). (Binding dom1, Binding dom) => dom a -> Maybe Integer is as general as its inferred signature a :: forall (dom :: * -> *) a. Binding dom => dom a -> Maybe Integer In an equation for ‘freeVars’: freeVars = \case { Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined } where (a, b) = (viewVar, viewBnd) tSvp.hs:20:5-31: error: … • Could not deduce (Binding dom1) from the context: Binding dom bound by the type signature for: freeVars :: Binding dom => AST dom a -> [Integer] at /tmp/tSvp.hs:14:1-49 or from: Binding dom2 bound by the inferred type for ‘b’: Binding dom2 => dom2 (a1 :-> b) -> Maybe Integer at /tmp/tSvp.hs:20:5-31 The type variable ‘dom1’ is ambiguous • When checking that the inferred type b :: forall k k1 (dom :: * -> *) a (dom1 :: * -> *) (a1 :: k) (b :: k1). (Binding dom1, Binding dom) => dom1 (a1 :-> b) -> Maybe Integer is as general as its inferred signature b :: forall k k1 (dom :: * -> *) (a :: k) (b :: k1). Binding dom => dom (a :-> b) -> Maybe Integer In an equation for ‘freeVars’: freeVars = \case { Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined } where (a, b) = (viewVar, viewBnd) Compilation failed. }}} Is this intentional? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Oddly all three work for me, in HEAD and the 8.0 branch, and GHC 8.0.1. Are you sure you've put in the right code? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Ah! It has something to do with the extensions I enabled in my `.ghci`: With {{{#!hs {-# Language GADTs,LambdaCase,TypeOperators,ViewPatterns #-} }}} it compiles just fine, but it fails when I add {{{#!hs {-# Language GADTs,LambdaCase,TypeOperators,ViewPatterns,NoMonomorphismRestriction #-} }}}s -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): With {{{#!hs {-# Language GADTs,LambdaCase,TypeOperators,ViewPatterns,ScopedTypeVariables#-} {-# Language TypeApplications #-} infixr :-> infixl 1 :$ data Full a data a :-> b data AST dom sig where Sym :: dom sig -> AST dom sig (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig class Binding dom where viewVar :: dom a -> Maybe Integer viewBnd :: dom (a :-> b) -> Maybe Integer freeVars :: forall dom a. Binding dom => AST dom a -> [Integer] freeVars = \case Sym (a -> Just v) -> [v] Sym (b -> Just v) :$ body -> undefined where (a, b) = (viewVar @dom, undefined) }}} it also gives the error {{{ /tmp/tPYo.hs:20:8: error: • Couldn't match expected type ‘dom (a1 :-> a) -> Maybe t1’ with actual type ‘t0’ because type variable ‘a1’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: :$ :: forall (dom :: * -> *) sig a. AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig, in a case alternative at /tmp/tPYo.hs:20:3-27 • In the pattern: b -> Just v In the pattern: Sym (b -> Just v) In the pattern: Sym (b -> Just v) :$ body • Relevant bindings include a :: dom a -> Maybe Integer (bound at /tmp/tPYo.hs:23:6) b :: t0 (bound at /tmp/tPYo.hs:23:9) freeVars :: AST dom a -> [Integer] (bound at /tmp/tPYo.hs:18:1) Failed, modules loaded: none. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah now I see. The offending where clause is equivalent to this: {{{ where t = (viewVar, vewBnd) a = case t of (a,b) -> a b = case t of (a,b) -> b }}} What type does `t` get? {{{ t :: forall d1 d2 a1 a2 b2. Binding d1, Binding d2) => (d1 a1 -> Maybe Integer, d2 (Fun a2 b2) -> Maybe Integer) }}} Now when we call `t` in the RHS of `a` we get the error message you see, because nothing fixes `d2` and hence we can't resolve `Binding d2` even though it is not in fact used. This doesn't arise when there is just one variable; try the same desugaring and you'll see. The monomorphism restriction means that we don't attempt to generalise over `Binding d1` etc, so none of this happens. I agree that this is perplexing, but I don't really know how to improve it. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): It may be fine as it is, but my intuition says I should be able to change {{{#!hs where a = xx b = yy }}} to {{{#!hs where (a, b) = (xx, yy) }}} Does it make any sense to treat/desugar `(a, b) = (xx, yy)` bindings as `x = xx; b = yy` or does that open a separate can of worms? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): It would just be another strange special case. What about {{{ (a,b) = id (xx, yy) }}} Does not sound attractive to me -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12542: Unexpected failure.. (bug?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Good point -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12542#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC