#9607: Type checking regression between GHC 7.6 and 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Indeed, and there is a good reason for that: when you call `rightUnit`, its unclear how to instantiate `n`; its type is indeed ambiguous. For example, if you write this {{{ rightUnit1 :: Tensor s -> Tensor (s ++ '[n, n]) ru1 = rightUnit }}} you might expect it to be accepted. After all, that ''is'' the type of `rightUnit`! But it's rejected thus: {{{ T9607.hs:34:7: Couldn't match type ‘s ++ '[n0, n0]’ with ‘s ++ '[n, n]’ NB: ‘++’ is a type function, and may not be injective The type variable ‘n0’ is ambiguous Expected type: Tensor s -> Tensor (s ++ '[n, n]) Actual type: Tensor s -> Tensor (s ++ '[n0, n0]) Relevant bindings include ru1 :: Tensor s -> Tensor (s ++ '[n, n]) (bound at T9607.hs:34:1) In the expression: rightUnit In an equation for ‘ru1’: ru1 = rightUnit }}} This perplexing behaviour is ruled out by the default of `-XNoAllowAmbiguousTypes`. However your example is useful because it shows an example where a function with an ambiguous type can nevertheless be called in an entirely unambiguous way. The call in `userightUnit` instantiates the type of `rightUnit` with (say) `s = ss` and `n = nn`. Now we get the following constraints: {{{ Tensor ss ~ Tensor [1] -- From the argument of rightUnit Tensor (ss ++ [nn, nn]) ~ Tensor [1,2,2] -- From the result of rightUnit }}} solving the first gives `ss ~ [1]`. Substituting in the second gives {{{ [1] ++ [nn,nn] ~ [1,2,2] }}} Now use the equations for `++` and you can see this is readily solved by `nn ~ 2`. In short, ''some'' calls to `rightUnit` will give rise to ambiguity, but not all. It's not clear what "better" behaviour might be. One thing I can think of is this: * Allow ambiguous user-written type signatures * But do not infer ambiguous types I.e. if you want a function to get an ambiguous type you must say so. See also #9587 Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9607: Type checking regression between GHC 7.6 and 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: invalid | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by jmccarty): Indeed, I'm guessing it was a bug that 7.6 accepted my program. I would argue that the type is not per se ambiguous, GHC just can't see it. `leftUnit` is precisely as ambiguous as `rightUnit`, but `leftUnit` is considered unambiguous (I think) because the type family application simplifies, making the signature `Tensor s -> Tensor (n ': n ': s)`, and I guess `':` is accepted as injective. In principle, if the argument and return types of rightUnit are instantiated to some type, then `n` can be instantiated to a unique type (but GHC would have to invert `(s ++)` to determine it!). I don't really understand the ambiguity check, but I think GHC wants to check that `(s ++ '[n0, n0]) ~ (s ++ '[n, n])` implies `n0 ~ n`? This is provably true, but I certainly don't expect GHC to construct the inductive proof of this fact. I was hoping the type family injectivity proposal would allow declaring such a fact (but again, I don't know that GHC could verify it). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9607: Programs that require AllowAmbiguousTypes in 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: invalid | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9607: Programs that require AllowAmbiguousTypes in 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by trevorcook): My apologies if I am off base, but I think I have an example. I'm making a visualization server that handles the rendering of 3d* graphics. The server listens for messages regarding "entity" primitives and current point of view. For every entity it adds it handshakes to the client with a unique id, so that the client can update the entity if needed. The basic service deals with primitive shapes, and the idea is to develop client services which can translate between higher level abstractions and the visualization primitives. For example, a plotting utility might be a client which exposes an "axes" primitive, which in turn relates to a set of visualization primitives used for tic marks, axis lines, and labels. I'm organizing the architecture to be based on the below Client and Server type classes. Clients create commands and further processing based on the responses to the commands. Servers listen to commands, do something, and eventually return responses. The classes attempt to separate out the key protocol/visualization components from the actual implementation. The forwarding action below pastes together clients and servers, and will hopefully be reusable for making concrete services based on different messaging technologies, and for implementations for different visualization domains. It seems to require AmbiguousTypes, though I don't understand why. {{{#!haskell {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE AllowAmbiguousTypes #-} module CSFwd where import VisServ.Base import Data.Monoid (mconcat,Monoid) -- | Imported from VisServ.Base --type family ComResp cmd -- |triggered by some data, trig, a client request yields a list of commands, cmd, -- and functions which consume the resulting response. class ClientAction cmd trig a where clientRequest :: trig -> [(cmd, ComResp cmd -> a)] -- |triggered by some command, cmd, a server does some reaction, react, and -- given subsequent data, a, (presumably somehow derived from react) will -- respond to the command, ComResp cmd. class ServerAction cmd react a where serverResponse :: cmd -> (react, a -> ComResp cmd) -- The idea with forwarding action hinges to a large part around the server response -- (a->c->d). The idea being that whatever implementation of this server will have -- some data, a, available which needs to be combined with, c, to yield data, d, -- necessary for a response to the original metaCmd request. The data, c, can be -- created based on replys to visualization commands So, given the input functions -- which create the client trigger and initial data b, this function handles the -- forwarding of visualization commands based on some other commands. forwardingAction :: forall a b c d trig metaCmd . ( Monoid c , ServerAction metaCmd (a->c->d) d , ClientAction VisCom trig (b->c) ) => (metaCmd -> a -> trig) -> (metaCmd -> b) -> metaCmd -> a -> ([VisCom],[VisResp] -> d, d -> ComResp metaCmd) forwardingAction toTrig tob metaCmd a = (cliCmds,servReact',cmdResp) where (servReact::(a->c->d),cmdResp::d -> ComResp metaCmd) = serverResponse metaCmd cmdActs :: [(VisCom,VisResp -> b -> c)] cmdActs = clientRequest . toTrig metaCmd $ a (cliCmds,replResps) = unzip cmdActs b = tob metaCmd replResp' :: [VisResp] -> c replResp' resps = mconcat $ zipWith (\f resp-> f resp b) replResps resps servReact' :: [VisResp] -> d servReact' resps = servReact a (replResp' resps) }}} Error: {{{ src/CSFwd.hs:33:21: Could not deduce (ClientAction VisCom trig (b -> c0)) arising from the ambiguity check for ‘forwardingAction’ from the context (Monoid c, ServerAction metaCmd (a -> c -> d) d, ClientAction VisCom trig (b -> c)) bound by the type signature for forwardingAction :: (Monoid c, ServerAction metaCmd (a -> c -> d) d, ClientAction VisCom trig (b -> c)) => (metaCmd -> a -> trig) -> (metaCmd -> b) -> metaCmd -> a -> ([VisCom], [VisResp] -> d, d -> ComResp metaCmd) at src/CSFwd.hs:(33,21)-(38,67) The type variable ‘c0’ is ambiguous In the ambiguity check for: forall a b c d trig metaCmd. (Monoid c, ServerAction metaCmd (a -> c -> d) d, ClientAction VisCom trig (b -> c)) => (metaCmd -> a -> trig) -> (metaCmd -> b) -> metaCmd -> a -> ([VisCom], [VisResp] -> d, d -> ComResp metaCmd) To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘forwardingAction’: forwardingAction :: forall a b c d trig metaCmd. (Monoid c, ServerAction metaCmd (a -> c -> d) d, ClientAction VisCom trig (b -> c)) => (metaCmd -> a -> trig) -> (metaCmd -> b) -> metaCmd -> a -> ([VisCom], [VisResp] -> d, d -> ComResp metaCmd) }}} *Technically not real 3D. I'm using some projective transforms to create 2D vector graphics based on the diagrams front end. I use a simple ordering over the transformed shapes to determine the order they are glued to the page. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9607: Programs that require AllowAmbiguousTypes in 7.8 -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by trevorcook): Thanks for the insight. So, this is bad design, and an instance where ambiguity was mistakenly sought in the wild. I was vaguely aware of the mistake, but thought using the ambiguity flag made it all fine. In summary, I was attempting to make a configurable, general purpose function, but giving no way for the user to control the configuration, i.e. which instances of the class constraints containing 'c' to use. Hence the ambiguity. A solution which doesn't require AllowAmbiguousTypes is to let the user specify the configuration by handing forwardingAction some data. Below, I have a similar function which effectively passes the 'ServerAction' method call wrapped in a data ServCfg. {{{#!hs newtype ServCfg st cmd resp c = ServCfg { runService :: st -> cmd ->(resp,c->ComResp cmd)} maybeFwdAction :: forall st cmd trig b c . (ClientAction trig VisCom b) => ServCfg st cmd (Maybe (trig, b->c)) c -> st -> cmd -> (Maybe ([VisCom],[VisResp] -> c), c -> ComResp cmd) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9607#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler