Opened 5 years ago
Last modified 17 months ago
#9607 new bug
Programs that require AllowAmbiguousTypes in 7.8
Reported by: | jstolarek | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.3 |
Keywords: | TypeFamilies | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
Jason McCarty reported on Haskell-cafe that this code used to work with GHC 7.6 but in GHC 7.8 it requires AllowAmbiguousTypes
:
-- The code below is simplified from code that computes a tensor product of -- a tensor with an identity matrix whose size is determined from the -- shapes of the input and output tensors. {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} --{-# LANGUAGE AllowAmbiguousTypes #-} module Tensors where import GHC.TypeLits type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat] type instance '[] ++ bs = bs type instance (a ': as) ++ bs = a ': (as ++ bs) data Tensor (s :: [Nat]) = Tensor -- content elided -- apparently GHC reduces (++) enough to see that n is determined leftUnit :: Tensor s -> Tensor ('[n, n] ++ s) leftUnit Tensor = Tensor -- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes rightUnit :: Tensor s -> Tensor (s ++ '[n, n]) rightUnit Tensor = Tensor -- also accepted without AllowAmbiguousTypes outsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n]) outsideUnit Tensor = Tensor useleftUnit :: Tensor '[1,1,2] useleftUnit = leftUnit Tensor -- type of Tensor is inferred userightUnit :: Tensor '[1,2,2] userightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided
Change History (10)
comment:1 Changed 5 years ago by
comment:2 Changed 5 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
So this is essentially a feature, not a bug? In that case I'll close this report as 'invalid'. I was puzzled because it used to work with 7.6.
comment:3 Changed 5 years ago by
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).
comment:4 Changed 5 years ago by
I'm going to re-open, because I'd like to collect examples of where ambiguity was actively sought in the wild. However I don't propose any action right now.
Simon
comment:5 Changed 5 years ago by
Summary: | Type checking regression between GHC 7.6 and 7.8 → Programs that require AllowAmbiguousTypes in 7.8 |
---|
comment:6 Changed 5 years ago by
Resolution: | invalid |
---|---|
Status: | closed → new |
Re-opening, as I believe it was Simon's intention to keep this one open (#comment:4)
comment:7 Changed 5 years ago by
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.
{-# 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.
comment:8 follow-up: 9 Changed 5 years ago by
I believe GHC is right to reject this program. Look at the type signature of 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)
Note that the c
type variable - the on GHC claims is ambiguous - appears only under type classes in the context. It does not appear in type of any argument nor the return type. This means that at the call site there might be no way to infer what type should the c
variable be.
comment:9 Changed 5 years ago by
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.
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)
comment:10 Changed 17 months ago by
Keywords: | TypeFamilies added |
---|
Indeed, and there is a good reason for that: when you call
rightUnit
, its unclear how to instantiaten
; its type is indeed ambiguous. For example, if you write thisyou might expect it to be accepted. After all, that is the type of
rightUnit
! But it's rejected thus: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 ofrightUnit
with (say)s = ss
andn = nn
. Now we get the following constraints:solving the first gives
ss ~ [1]
. Substituting in the second givesNow use the equations for
++
and you can see this is readily solved bynn ~ 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:
I.e. if you want a function to get an ambiguous type you must say so.
See also #9587
Simon