Opened 5 years ago

Last modified 15 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 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

comment:2 Changed 5 years ago by jstolarek

Resolution: invalid
Status: newclosed

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 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).

comment:4 Changed 5 years ago by simonpj

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 rwbarton

Summary: Type checking regression between GHC 7.6 and 7.8Programs that require AllowAmbiguousTypes in 7.8

comment:6 Changed 5 years ago by jstolarek

Resolution: invalid
Status: closednew

Re-opening, as I believe it was Simon's intention to keep this one open (#comment:4)

comment:7 Changed 4 years ago 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.

{-# 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 Changed 4 years ago by jstolarek

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 in reply to:  8 Changed 4 years ago 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.

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 15 months ago by RyanGlScott

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.