- ghc-tickets - Haskell.org

[GHC] #10450: RankNTypes type check on pattern match of "let" behaves different from "case"
by GHC 19 Apr '17

19 Apr '17

#10450: RankNTypes type check on pattern match of "let" behaves different from "case" -------------------------------------+------------------------------------- Reporter: sjcjoosten | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 (Type checker) | Operating System: Unknown/Multiple Keywords: RankNTypes | Type of failure: GHC rejects Architecture: | valid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- When pattern matching, "let/where" and "case" have different behaviours. I believe this to be a bug, and my hope is that all of the following should be accepted. Currently, this is accepted (a version using 'where' instead of 'let' type-checks too): {{{#!hs {-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Main where data Phantom x = Phantom Int deriving Show foo :: forall y. (forall x. (Phantom x)) -> Phantom y foo (Phantom x) = Phantom (x+1) -- trying to map foo over a list, this is the only way I can get it to work typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap intList = case intList of [] -> [] _ -> let (phead:ptail) = intList in foo phead : typeAnnotatedMap ptail }}} The following are not accepted: {{{#!hs typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap intList = case intList of [] -> [] (phead:ptail) -> foo phead : typeAnnotatedMap ptail typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap [] = [] typeAnnotatedMap (phead:ptail) = foo phead : typeAnnotatedMap ptail }}} The switches "ImpredicativeTypes" and "NoImpredicativeTypes" only change GHC's behaviour in the following example, for which I understand (but don't like) that it is not accepted, its error message is fine: {{{#!hs typeAnnotatedMap :: (forall x. [Phantom x]) -> [Phantom y] typeAnnotatedMap lst = map foo lst }}} Tested this on 7.8.2. Version 7.6.3 and 7.4.2 seem to behave the same. Sorry for not testing this on the latest version. Should this not be a bug, it would help if the type checker would somehow point me in the direction of the solution (first version) when I write any one of the 'problem cases'. The current type error is something like: {{{ Couldn't match type ‘x0’ with ‘x’ because type variable ‘x’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: [Phantom x] }}} More helpful would be something like: {{{ Your pattern match bound the following types to a shared skolem variable: ptail :: [Phantom x0] (bound at rankNtest.hs:11:25) phead :: Phantom x0 (bound at rankNtest.hs:11:19) You may have intended to use a "let" or "where" pattern-match instead. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10450> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #13582: Confusing error message with multiparameter type classes.
by GHC 19 Apr '17

19 Apr '17

#13582: Confusing error message with multiparameter type classes. -------------------------------------+------------------------------------- Reporter: | Owner: (none) facundo.dominguez | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: type-checking | Operating System: Unknown/Multiple errors | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program {{{ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} import Data.Typeable class First a b c | c -> b where first :: c -> a -> b class Second a b where second :: a -> b instance (Typeable b, First a b c) => Second a c where second = undefined main :: IO () main = print (second (9 :: Int) :: Int) }}} produces the following error message {{{ $ runghc-8.0.2 t.hs t.hs:18:15: error: • No instance for (Typeable b0) arising from a use of ‘second’ • In the first argument of ‘print’, namely ‘(second (9 :: Int) :: Int)’ In the expression: print (second (9 :: Int) :: Int) In an equation for ‘main’: main = print (second (9 :: Int) :: Int) }}} Note that the message does not explain where `b0` comes from. ghc-7.8.3 produced a better error message: {{{ $ runghc-7.8.3 t.hs t.hs:18:15: No instance for (First Int b Int) arising from a use of ‘second’ In the first argument of ‘print’, namely ‘(second (9 :: Int) :: Int)’ In the expression: print (second (9 :: Int) :: Int) In an equation for ‘main’: main = print (second (9 :: Int) :: Int) }}} Doing slight modifications changes the error message that ghc-8.0.2. e.g. {{{ - instance (Typeable b, First a b c) => Second a c where + instance (First a b c, Typeable b) => Second a c where }}} gives the same error as ghc-7.8.3. In a big program the current error is very puzzling. Is ghc picking the wrong error to show? Could it print more errors perhaps? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13582> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 6

Re: [GHC] #6018: Injective type families
by GHC 19 Apr '17

19 Apr '17

#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature request | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.4.1 Resolution: fixed | Keywords: TypeFamilies, | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: T6018, | T6018fail, T6018rnfail, T6018th, | T6018failclosed1, T6018failclosed2, | T6018ghci, T6018ghcifail, | T6018ghcirnfail Blocked By: | Blocking: Related Tickets: #4259, #10832, | Differential Rev(s): Phab:D202 #10833 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies, Injective => TypeFamilies, InjectiveFamilies -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:120> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

Re: [GHC] #4259: Relax restrictions on type family instance overlap
by GHC 19 Apr '17

19 Apr '17

#4259: Relax restrictions on type family instance overlap -------------------------------------+------------------------------------- Reporter: lilac | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 6.12.1 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8423 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, InjectiveFamilies -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/4259#comment:38> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #10227: Type checker cannot deduce type
by GHC 19 Apr '17

19 Apr '17

#10227: Type checker cannot deduce type -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- When using closed type families the type checker does not use all the information that the closedness condition implies. In the following module the type checker fails to deduce the type for `f`. But lets start with `descrIn` since it has the same problem. The deduced type is `(D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d`. But it is (to quote Simon PJ) plain as a pikestaff that `D d Double ~ Bool` can only hold if `d ~ In`, since there are only two equations and it cannot be the second. Similar reasoning can be used to deduce all the commented out type signatures. {{{#!hs {-# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #-} module Main(main) where import Data.Maybe data InOut = In | Out type family D (d :: InOut) a where D 'In a = Bool D 'Out a = a data Descr d = Descr { abc :: D d Bool, def :: D d Double, ghi :: D d (Maybe String) } --descrIn :: Descr 'In descrIn = Descr { abc = False, def = True, ghi = True } --f :: Descr 'Out -> Double f Descr{..} = def + read (fromMaybe "0" ghi) --g :: Descr 'In -> Descr 'Out g d = Descr { abc = if abc d then True else False, def = if def d then 1234 else 0, ghi = if ghi d then Just "3008" else Nothing } main :: IO () main = do print $ f $ g descrIn }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10227> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 4

[GHC] #13571: Injective type family syntax accepted without TypeFamilyDependencies
by GHC 19 Apr '17

19 Apr '17

#13571: Injective type family syntax accepted without TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 (Parser) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple Injective | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program compiles fine although it names the result type variable, which is a piece of syntax that should only be available with `TypeFamilyDependencies` (injective type families): {{{#!haskell {-# LANGUAGE TypeFamilies #-} module Foo where type family F a = r where F a = a }}} If I say: {{{#!haskell type family F a = r | r -> a where F a = a }}} only then the definition is rejected. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13571> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 1

[GHC] #11511: Type family producing infinite type accepted as injective
by GHC 19 Apr '17

19 Apr '17

#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple Injective | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- A question came up during discussion at University of Wrocław: {{{#!hs type family F a = r | r -> a where F a = [F a] }}} Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible. This is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11511> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

Re: [GHC] #7259: Eta expansion of products in System FC
by GHC 19 Apr '17

19 Apr '17

#7259: Eta expansion of products in System FC -------------------------------------+------------------------------------- Reporter: simonpj | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.1 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: | -------------------------------------+------------------------------------- Changes (by edsko): * cc: edsko (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7259#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 0

[GHC] #13588: Simplify StgCase when all alternatives are the case binder
by GHC 19 Apr '17

19 Apr '17

#13588: Simplify StgCase when all alternatives are the case binder -------------------------------------+------------------------------------- Reporter: nomeata | Owner: (none) Type: task | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- Nudged by rwbarton, simponpj writes in ticket:13536#comment:16: Yes. It's really {{{ case e of w { p1 -> w; ...; pn -> w } ===> e }}} (Core has a more general version involving strictness on x.) I don't know how much it happens in practice. It would not be hard to include this in StgCse though. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13588> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #13569: Optimise code-gen for field-updates of large products
by GHC 18 Apr '17

18 Apr '17

#13569: Optimise code-gen for field-updates of large products -------------------------------------+------------------------------------- Reporter: hvr | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (CodeGen) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's something we talked about last year which I wanted to look into but then got distracted (but I'm writing this one up now so it doesn't get lost again): Consider large field updates such as {{{#!hs module BigRec where data T = C { fld01 :: !Int , fld02 :: !Int , fld03 :: Int , fld04 :: Int , fld05 :: Int , fld06 :: Int , fld07 :: Int , fld08 :: Int , fld09 :: Int , fld10 :: Int , fld11 :: Int , fld12 :: Int , fld13 :: Int , fld14 :: Int , fld15 :: Int , fld16 :: Int , fld17 :: Int , fld18 :: Int , fld19 :: Int } inc01 x = x { fld01 = (fld01 x) + 1 } inc0102 x = x { fld01 = (fld01 x) + 1, fld02 = (fld02 x) + 1 } }}} These get translated into long chains of assignments, which in turn result in respectively long chains of register<->memory move instructions being generated by the NCG {{{#!c BigRec.inc0102_entry() // [R2] { [(c1em, block_c1em_info: const 0; const 31;), (c1ep, BigRec.inc0102_info: const 4294967301; const 0; const 15;)] } {offset c1ep: if ((Sp + -8) < SpLim) goto c1ez; else goto c1eA; c1ez: // nop R1 = BigRec.inc0102_closure; call (I64[BaseReg - 8])(R2, R1) args: 8, res: 0, upd: 8; c1eA: I64[Sp - 8] = block_c1em_info; R1 = R2; Sp = Sp - 8; if (R1 & 7 != 0) goto c1em; else goto c1en; c1en: call (I64[R1])(R1) returns to c1em, args: 8, res: 8, upd: 8; c1em: Hp = Hp + 160; if (Hp > I64[BaseReg + 856]) goto c1eD; else goto c1eC; c1eD: I64[BaseReg + 904] = 160; // nop call stg_gc_unpt_r1(R1) returns to c1em, args: 8, res: 8, upd: 8; c1eC: _s15F::P64 = P64[R1 + 7]; _s15G::P64 = P64[R1 + 15]; _s15H::P64 = P64[R1 + 23]; _s15I::P64 = P64[R1 + 31]; _s15J::P64 = P64[R1 + 39]; _s15K::P64 = P64[R1 + 47]; _s15L::P64 = P64[R1 + 55]; _s15M::P64 = P64[R1 + 63]; _s15N::P64 = P64[R1 + 71]; _s15O::P64 = P64[R1 + 79]; _s15P::P64 = P64[R1 + 87]; _s15Q::P64 = P64[R1 + 95]; _s15R::P64 = P64[R1 + 103]; _s15S::P64 = P64[R1 + 111]; _s15T::P64 = P64[R1 + 119]; _s15U::P64 = P64[R1 + 127]; _s15V::P64 = P64[R1 + 135]; _s15X::I64 = I64[R1 + 151] + 1; _s15W::I64 = I64[R1 + 143] + 1; I64[Hp - 152] = BigRec.C_con_info; P64[Hp - 144] = _s15F::P64; P64[Hp - 136] = _s15G::P64; P64[Hp - 128] = _s15H::P64; P64[Hp - 120] = _s15I::P64; P64[Hp - 112] = _s15J::P64; P64[Hp - 104] = _s15K::P64; P64[Hp - 96] = _s15L::P64; P64[Hp - 88] = _s15M::P64; P64[Hp - 80] = _s15N::P64; P64[Hp - 72] = _s15O::P64; P64[Hp - 64] = _s15P::P64; P64[Hp - 56] = _s15Q::P64; P64[Hp - 48] = _s15R::P64; P64[Hp - 40] = _s15S::P64; P64[Hp - 32] = _s15T::P64; P64[Hp - 24] = _s15U::P64; P64[Hp - 16] = _s15V::P64; I64[Hp - 8] = _s15W::I64; I64[Hp] = _s15X::I64; R1 = Hp - 151; }}} This happens in a few places inside GHC's source-tree (where we have large-ish products, such as DynFlags where we update single fields), which is where I noticed this while looking at generated ASM output. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13569> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8