August 2013 - Glasgow-haskell-users

match_co: needs more cases
by Evan Laforge 07 Nov '13

07 Nov '13

I made some strictifying changes and started getting this msg from ghc: match_co: needs more cases vector-0.10.0.1:Data.Vector.Generic.Mutable.MVector{tc r46} (Sym <(vector-0.10.0.1:Data.Vector.TFCo:R:MutableVector{tc r45})>) <main:Util.TimeVectorStorable.Sample{tc r4e} y{tv a4lK} [tv]> It's not just TimeVectorStorable.Sample (which is indeed stored in Data.Vectors), we also have some mysterious compiler-generated symbols: match_co: needs more cases vector-0.10.0.1:Data.Vector.Generic.Mutable.MVector{tc rQA} (Sym <(vector-0.10.0.1:Data.Vector.TFCo:R:MutableVector{tc rQz})>) <a{tv a6IH} [tv]> I assume this is harmless, but I didn't see any other references to this error on the web or on the ghc trac so maybe it's new?

4 5

Question about correct GHC-API use for type checking (or zonking, or tidying)
by p.k.f.holzenspies＠utwente.nl 04 Sep '13

04 Sep '13

Dear GHC-ers, I'm working on building an interactive environment around the composition of expressions. Users can type in (i.e. give strings of) expressions and can then use these expressions to produce other expressions. I'm close to having a working GHC-API binding for this. The resulting types, however, still contain some things I don't quite understand. Any help would be appreciated. Below, I've included the function exprFromString which should parse, rename and typecheck strings to Id-things and give their type (although, ideally, the idType of said Id-thing should be the same as the type returned). This function lives in the IA (InterActive) monad; a monad that is a GhcMonad and can lift monadic computations in TcM into itself using liftTcM (which uses the initTcPrintErrors and setInteractiveContext functions similarly to TcRnDriver.tcRnExpr). Near the end of the function, debugging output is produced. This output confuses me slightly. Here is the output for the three inputs "map (+1) [1..10]", "5" and "\\x -> x": map (+1) [1..10] pre-zonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i] post-zonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i] idType: [b_c] tidied: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i] 5 pre-zonk: forall a. GHC.Num.Num a_d => t_c post-zonk: forall a. GHC.Num.Num a_d => t_c idType: a_b tidied: forall a. GHC.Num.Num a_d => t_c \x -> x pre-zonk: forall t. t_e post-zonk: forall t. t_e idType: forall t. t -> t tidied: forall t. t_e The zonking and tidying part of the type-checking process are still a bit unclear to me and I suspect the problems arise there. It looks to me that the type variables in the quantifications are different ones from those in the pi/rho-types. I had expected the types to only contain the variables over which they are quantified, so e.g. in the map-example, I had expected "forall b . (GHC.Enum.Enum b, GHC.Num.Num b) => [b]" Can anyone explain what I'm missing? Regards, Philip exprFromString :: String -> IA (Id,Type) exprFromString str = do dfs <- getDynFlags let pp = showSDoc dfs . ppr pst <- mkPState dfs buf <$> newRealSrcLoc {- Parse -} (loc,rdr_expr) <- case unP parseStmt pst of PFailed span err -> throwOneError (mkPlainErrMsg dfs span err) POk pst' (Just (L l (ExprStmt rdr_expr _ _ _))) -> do logWarningsReportErrors (getMessages pst') return (l,rdr_expr) POk pst' thing -> throw $ maybe EmptyParse (const NonExpressionParse) thing liftTcM $ do fresh_it <- freshName loc str {- Rename -} (rn_expr, fvs) <- checkNoErrs $ rnLExpr rdr_expr {- Typecheck -} let binds = mkBinds fresh_it rn_expr fvs (((_bnds,((_tc_expr,res_ty),id)),untch),lie) <- captureConstraints . captureUntouchables $ tcLocalBinds binds ((,) <$> tcInferRho rn_expr <*> tcLookupId fresh_it) ((qtvs, dicts, _bool, _evbinds), lie_top) <- captureConstraints $ simplifyInfer True False [(fresh_it, res_ty)] (untch,lie) let all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty) say str say $ " pre-zonk: " ++ pp all_expr_ty zonkTcType all_expr_ty say $ " post-zonk: " ++ pp all_expr_ty say $ " idType: " ++ pp (idType id) say $ " tidied: " ++ pp (tidyTopType all_expr_ty) return (id,all_expr_ty) where say = liftIO . putStrLn buf = stringToStringBuffer str freshName loc str = (\u -> mkInternalName u name loc) <$> newUnique where name = mkOccNameFS varName $ fsLit $ "it" ++ show (lineOf loc) isVarChar c = isAlphaNum c || c == '_' || c == '\'' lineOf (RealSrcSpan s) = srcSpanStartLine s lineOf _ = -1 mkBinds :: Name -> LHsExpr Name -> FreeVars -> HsLocalBinds Name mkBinds nm e@(L l _) fvs = HsValBinds $ ValBindsOut [(NonRecursive, unitBag the_bind)] [] where the_bind = L l (mkTopFunBind (L l nm) [mkMatch [] e emptyLocalBinds]) { bind_fvs = fvs }

2 5

32-bit libs required for 64-bit install
by Yitzchak Gale 28 Aug '13

28 Aug '13

I had trouble installing the generic 64-bit Linux tarball for 7.6.3. With some help from Ian, who pointed out that the problem was related to ld-linux.so, I finally figured out the root of the problem: the installation requires *both* the 64-bit and 32-bit versions of libc6 plus deps to be available. Once the installation was complete, I could then remove the 32-bit libs and ghc still seems to work. It appears that the 32-bit libs are only required for some of the auxiliary executables that come with the tarball, such as ghc-pwd. Is there any reason in principle that we only allow 64-bit GHC to be installed on multiarch Linux? That seems like a rather arbitrary restriction. In the meantime, something ought to be said about this on the download page. More details: the target system for the installation in my case was an up-to-date Ubuntu 12.04 LTS (precise) amd64 headless server running in a VMware containter. Thanks, Yitz

3 2

TypeHoles behaviour
by Andres Löh 28 Aug '13

28 Aug '13

Hi. I've just started playing with TypeHoles. (I'm writing some Haskell course materials and would like to use them from the very beginning once they become available.) However, I must say that I don't understand the current notion of "relevance" that seems to determine whether local bindings are included or not. The current rule seems to be that bindings are included only if the intersection between the type variables their types involve and the type variables in the whole is non-empty. However, I think this is confusing. Let's look at a number of examples: > f1 :: Int -> Int -> Int > f1 x y = _ Found hole ‛_’ with type: Int In the expression: _ In an equation for ‛f1’: f1 x y = _ No bindings are shown. > f2 :: a -> a -> a > f2 x y = _ Found hole ‛_’ with type: a Where: ‛a’ is a rigid type variable bound by the type signature for f2 :: a -> a -> a at List.hs:6:7 Relevant bindings include f2 :: a -> a -> a (bound at List.hs:7:1) x :: a (bound at List.hs:7:4) y :: a (bound at List.hs:7:6) In the expression: _ In an equation for ‛f2’: f2 x y = _ Both x and y (and f2) are shown. Why should this be treated differently from f1? > f3 :: Int -> (Int -> a) -> a > f3 x y = _ Found hole ‛_’ with type: a Where: ‛a’ is a rigid type variable bound by the type signature for f3 :: Int -> (Int -> a) -> a at List.hs:9:7 Relevant bindings include f3 :: Int -> (Int -> a) -> a (bound at List.hs:10:1) y :: Int -> a (bound at List.hs:10:6) In the expression: _ In an equation for ‛f3’: f3 x y = _ Here, y is shown, but x isn't, even though y has to be applied to an Int in order to produce an a. Of course, it's possible to obtain an Int from elsewhere ... f4 :: a -> (a -> b) -> b f4 x y = _ Found hole ‛_’ with type: b Where: ‛b’ is a rigid type variable bound by the type signature for f4 :: a -> (a -> b) -> b at List.hs:12:7 Relevant bindings include f4 :: a -> (a -> b) -> b (bound at List.hs:13:1) y :: a -> b (bound at List.hs:13:6) In the expression: _ In an equation for ‛f4’: f4 x y = _ Again, only y is shown, and x isn't. But here, the only sane way of filling the hole is by applying "y" to "x". Why is one more relevant than the other? f5 x y = _ Found hole ‛_’ with type: t2 Where: ‛t2’ is a rigid type variable bound by the inferred type of f5 :: t -> t1 -> t2 at List.hs:15:1 Relevant bindings include f5 :: t -> t1 -> t2 (bound at List.hs:15:1) In the expression: _ In an equation for ‛f5’: f5 x y = _ Neither x and y are included without a type signature. Even though all of the above types are admissible, which would convince GHC that one or even all may be relevant. IMHO, this isn't worth it. It's a confusing rule. Just include all local bindings in the output, always. That's potentially verbose, but easy to understand. It's also potentially really helpful, because it trains beginning programmers to see what types local variables get, and it's a way to obtain complex types of locally bound variables for expert programmers. It's also much easier to explain. It should be easier to implement, too :) Could we please change it? Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

5 5

Fwd: New restrictions to open type families
by Akio Takano 23 Aug '13

23 Aug '13

(I forgot to send to the list, trying again) Thank you very much for your detailed explanation! On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg <eir(a)cis.upenn.edu>wrote: > This is a good question. Happily, there are at least two decent answers. > > 1) We're not sure that this problem cannot cause a segfault… it's just > that we've been unable to produce one when trying. Perhaps we haven't tried > hard enough. > I successfully constructed such an example. https://github.com/takano-akio/type-family-overlap - Akio

3 3

New restrictions to open type families
by Akio Takano 23 Aug '13

23 Aug '13

Hi, Looking at the ticket [1] and a draft paper linked there [2] , I learned that in GHC 7.8, two type family instances are considered overlapping if the argument lists unify in the presence of infinite types. My question is, why is this restriction necessary? A footnote in the paper states that it was not possible with GHC 7.6 to actually exploit the inconsistency. Would it be difficult to solve the problem by making this behaviour part of the specification, rather than accepting fewer programs? [1] http://ghc.haskell.org/trac/ghc/ticket/8154 [2] http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf Regards, Takano Akio

3 2

Liberalising IncoherentInstances
by Simon Peyton-Jones 19 Aug '13

19 Aug '13

Friends I've realised that GHC's -XIncoherentInstances flag is, I think, over-conservative. I propose to liberalise it a bit. This email describes the issue. Please yell if you think this is a bad idea. Simon Suppose we have class C a where { op :: a -> String } instance C [a] where ... instance C [Char] where ... f :: [b] -> String f xs = "Result:" ++ op xs With -XOverlappingInstances, but without -XIncoherentInstances, f won't compile. Reason: if we call 'f' at Char (e.g. f "foo") then you might think we should use instance C [Char]. For example, if we inlined 'f' at the call site, to get ("Result:" ++ op "foo"), we certainly then would use the C [Char] instance, giving perhaps different results. If we accept the program as-is, we'll permanently commit 'f' to using the C [a] instance. The -XIncoherentInstances flag says "Go ahead and use an instance, even if another instance might become relevant if you were to specialise or inline the enclosing function." The GHC user manual gives a more precise spec [1]. Now consider this class D a b where { opD :: a -> b -> String } instance D Int b where ... instance D a Int where ... g (x::Int) = opD x x Here 'g' gives rise to a constraint (D Int Int), and that matches two instance declarations. So this is rejected regardless of flags. We can fix it up by adding instance D Int Int where ... but this is pretty tiresome in cases where it really doesn't matter which instance you choose. (And I have a use-case where it's more than tiresome [2].) The underlying issue is similar to the previous example. Before, there was *potentially* more than one way to generate evidence for (C [b]); here there is *actually* more than one instance. In both cases the dynamic semantics of the language are potentially affected by the choice -- but -XIncoherentInstnaces says "I don't care". So the change I propose to make IncoherentInstances to pick arbitrarily among instances that match. More precisely, when trying to find an instance matching a target constraint (C tys), a) Find all instances matching (C tys); these are the candidates b) Eliminate any candidate X for which another candidate Y is strictly more specific (ie Y is a substitution instance of X), if either X or Y was complied with -XOverlappingInstances c) Check that any non-candidate instances that *unify* with (C tys) were compiled with -XIncoherentInstances d) If only one candidate remains, pick it. Otherwise if all remaining candidates were compiled with -XInccoherentInstances, pick an arbitrary candidate All of this is precisely as now, except for the "Otherwise" part of (d). One could imagine different flags for the test in (c) and (d) but I really don't think it's worth it. Incidentally, I think it'd be an improvement to localise the Overlapping/Incoherent flags to particular instance declarations, via pragmas, something like instance C [a] where {-# ALLOW_OVERLAP #-} op x = .... Similarly {-# ALLOW_INCOHERENT #-}. Having -XOverlappingInstances for the whole module is a bit crude., and might be missed when looking at an instance. How valuable would this be? [1] http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensio… [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers

7 12

Marking type constructor arguments as nominal (e.g. Set)
by Joachim Breitner 19 Aug '13

19 Aug '13

Hi, now that roles are in HEAD, I could play around a bit with it. They were introduced to solve the unsoundness of newtype deriving, but there is also the problem of abstraction: If I define a set type based on an ord instance, e.g. data Set a = Set a -- RHS here just for demonstration the I don’t want my users to replace a "Set Int" by a "Set (Down Int)", even though the latter is a newtype of the former. This can be prevented by forcing the role of "a" to be Nominal (and not Representational, as it is by default). What I just noticed is that one does not even have to introduce new syntax for it, one can just use: type family NominalArg x type instance (NominalArg x) = x data Set' a = Set' (NominalArg a) and get different roles; here the excerpt from --show-iface (is there an easier way to see role annotations): 5b7b2f7c3883ef0d9fc7934ac56c4805 data Set a@R [..] 8e15d783d58c18b8205191ed3fd87e27 data Set' a@N The type family does not get into the way, e.g. conv (Set a) = Set' a works as usual. (I now also notice that the parser actually supports role annotations... but still a nice, backward-compatible trick here). Greetings, Joachim -- Joachim “nomeata” Breitner mail(a)joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata(a)joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata(a)debian.org

4 5

Question about `compileToCoreModule`
by Daniel F 19 Aug '13

19 Aug '13

Hi, everyone, I have a question about `compileToCoreModule` function from the GHC module. I noticed that the following code not just outputs the Core code, but also produces object files and a linked executable (in case when 'test.hs' is a program): --------------------------- module Main where import DynFlags import GHC import GHC.Paths import MonadUtils import Outputable main = defaultErrorHandler defaultFatalMessager defaultFlushOut $ do runGhc (Just libdir) $ do dflags <- getSessionDynFlags setSessionDynFlags dflags cm <- compileToCoreModule "test.hs" output cm -- | Outputs any value that can be pretty-printed using the default style output :: (GhcMonad m, MonadIO m) => Outputable a => a -> m () output a = do dfs <- getSessionDynFlags let style = defaultUserStyle let cntx = initSDocContext dfs style liftIO $ print $ runSDoc (ppr a) cntx ----------------------------- I thought this was strange and looked up the source of 'compileToCoreModule', and indeed, it calls 'load LoadAllTargets'. So my question is, why is it necessary to do so? I had the impression that compiling Haskell to Core is a step that precedes compiling to the actual binary. NB: I tried setting `ghcLink' and `hscTarget' options in dynflags to `NoLink' and `HscNothing' respectively, but that resulted in somewhat weird Core: $ cat test.hs module Test (test) where test :: Int test = 123 test2 :: String test2 = "Hi" $ ./testcore %module main:Test (Safe-Inferred) [(reF, Identifier `Test.test')] Test.test :: GHC.Types.Int [LclIdX] Test.test = GHC.Types.I# 123 $ ./testcore-nolinknothing %module main:Test (Safe-Inferred) [] Thanks. -- Sincerely yours, -- Daniil Frumin

1 0

Private classes
by Joachim Breitner 17 Aug '13

17 Aug '13

Hi, for some reason I was under the impression that if I don’t export the methods of a class, then no user of my module can create instances. But I was wrong and in fact they can; the methods will just all be bound to "error ...". Is there really no way to create a class so that no-one else can create any instances? Greetings, Joachim -- Joachim “nomeata” Breitner mail(a)joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata(a)joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata(a)debian.org

4 5