[GHC] #15470: Record projections with ambiguous types
#15470: Record projections with ambiguous types -------------------------------------+------------------------------------- Reporter: sweirich | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code fails {{{ {-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, RankNTypes, AllowAmbiguousTypes #-} module TypeLambda where data Fun a b type family App (f :: Fun t k) (x :: t) :: k data MONAD m = MONAD { return :: forall a. a -> App m a , (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b } }}} with the error message {{{ TypeLambda.hs:12:5: error: • Couldn't match type ‘App m b0’ with ‘App m b’ Expected type: App m a -> (a -> App m b) -> App m b Actual type: App m a -> (a -> App m b0) -> App m b0 NB: ‘App’ is a non-injective type family The type variable ‘b0’ is ambiguous • In the expression: (>>=) In an equation for ‘TypeLambda.>>=’: (TypeLambda.>>=) MONAD {>>= = (>>=)} = (>>=) • Relevant bindings include (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b (bound at TypeLambda.hs:12:5) | 12 | , (>>=) :: forall a b. App m a -> (a -> App m b) -> App m b | ^^^^^ Failed, no modules loaded. }}} However, with ScopedTypeVariables and TypeApplications, it is possible to define the projections: {{{ data MONAD2 m = MONAD2 (forall a. a -> App m a) (forall a b. App m a -> (a -> App m b) -> App m b) bind :: forall b a m. MONAD2 m -> App m a -> (a -> App m b) -> App m b bind (MONAD2 _ b) = b @a @b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15470 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15470: Record projections with ambiguous types -------------------------------------+------------------------------------- Reporter: sweirich | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I thought that visible type applications would work too, so I tried it (diff below). Alas it turns out that we give record selectors ''nested'' forall types. For example from {{{ data T m = MkT { fld :: forall a. m a -> m a } }}} we get the selector: {{{ fld :: forall m. T m -> (forall a. m a -> m a) }}} So we can't use scoped type variables from the signature to instantiate in the RHS, ike this {{{ fld :: forall m. T m -> (forall a. m a -> m a) fld (MkT x) = x @ a -- No }}} Bother. Maybe we can change this assumption, and put all the foralls (and constraints) at the top of record selectors? I'm not sure of the consequences of doing so. The choice is made in the definition of `sel_ty` in `TcTyDecls.mkOneRecordSelector`. It affects user code. For example, do we write `fld @IO r @Int` or `fld @IO @Int r`? So it's be a breaking change. I'm not sure I see any other solution, alas. Richard, Mr VTA? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15470#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15470: Record projections with ambiguous types -------------------------------------+------------------------------------- Reporter: sweirich | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I forgot to put in the diff {{{ modified compiler/typecheck/TcTyDecls.hs @@ -893,7 +893,7 @@ mkOneRecordSelector all_cons idDetails fl | otherwise = map mk_match cons_w_field ++ deflt mk_match con = mkSimpleMatch (mkPrefixFunRhs sel_lname) [L loc (mk_sel_pat con)] - (L loc (HsVar noExt (L loc field_var))) + match_body mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields) rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing } rec_field = noLoc (HsRecField @@ -905,6 +905,19 @@ mkOneRecordSelector all_cons idDetails fl sel_lname = L loc sel_name field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc + match_body = L loc (HsVar noExt (L loc field_var)) +{- + match_body = foldl app_tv (L loc (HsVar noExt (L loc field_var))) field_tvs + + app_tv :: LHsExpr GhcRn -> TyVar -> LHsExpr GhcRn + app_tv hs_fun tv = L loc (HsAppType (mk_tv_ty tv) hs_fun) + + mk_tv_ty :: TyVar -> LHsWcType GhcRn + mk_tv_ty tv = mkEmptyWildCardBndrs $ L loc $ + HsTyVar noExt NotPromoted $ + L loc (getName tv) +-} }}} If you try commenting out the definition of `match_body` and replacing it with the one that is commented out in this diff, you get my attempt. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15470#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15470: Record projections with ambiguous types -------------------------------------+------------------------------------- Reporter: sweirich | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm a bit leery about changing the order of type variables just to support this one use case, especially since if we had the ability to bind type variables in lambdas, then we could implement these record projections without the need to change the original types: {{{#!hs type family F a data T a = MkT (forall a. F a) fld :: T -> (forall a. F a) fld (MkT x) = (\@a -> x @a) }}} Moreover, this type-variable-reordering hack really only works in one direction. That is to say, you can define record selectors since the position of the `forall` allows you to float those type variables to the front, but you can't define a synonym for the constructor itself, like so: {{{#!hs mkT :: (forall a. F a) -> T mkT = ??? }}} Here, we can't float the `a` to the front, so we're left without a way to implement this. With type variables in lambdas, we could, however: {{{#!hs mkT :: (forall a. F a) -> T mkT x = T (\@a -> x @a) }}} Of course, I'm speculating a bit here and assuming that the ambiguity check won't kick in on the examples above. (I have no way of knowing this, since type-variables-in-lambdas aren't yet implemented.) But it seems like it could be a viable alternative. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15470#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC