[GHC] #9733: Strange errors when using type families as parameters
GHC
ghc-devs at haskell.org
Tue Oct 28 13:13:45 UTC 2014
#9733: Strange errors when using type families as parameters
-------------------------------------+-------------------------------------
Reporter: crockeea | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.3
Resolution: duplicate | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: GHC | Blocked By:
rejects valid program | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Description changed by crockeea:
Old description:
> I seem to have found a dark corner of GHC. In the process of finding a
> minimal example, I found a few different ways to trigger a bug. I'm
> assuming they are all related.
>
> == Example 1 ==
> I started off with a GADT parameterized by a type list:
>
> {{{#!haskell
> {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
>
> module Foo where
>
> type TList = '[Float, Double]
>
> type family PrevElt (xs :: [*]) (a :: *) :: * where
> PrevElt (b ': a ': xs) a = b
> PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
>
> data FooList :: ([*] -> * -> *) where
> Bar :: FooList prevrp ((PrevElt prevrp rp) -> rp)
>
> test1 :: FooList TList ((PrevElt TList rp) -> rp)
> test1 = Bar
> }}}
> which compiles as expected.
>
> If I make a syntactic change and parameterize the GADT with the type
> family rather than the type list:
>
> {{{#!hs
> {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
>
> module Foo where
>
> type TList = '[Float, Double]
>
> type family PrevElt (xs :: [*]) (a :: *) :: * where
> PrevElt (b ': a ': xs) a = b
> PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
>
> data FooTF :: ((* -> *) -> * -> *) where
> Bar :: FooTF prevrp ((prevrp rp) -> rp)
>
> test2 :: FooTF (PrevElt TList) ((PrevElt TList rp) -> rp)
> test2 = Bar
> }}}
> I get a non-sensical error:
> {{{
> Foo.hs:15:9:
> Couldn't match type `PrevElt TList rp' with `PrevElt TList rp'
> NB: `PrevElt' is a type function, and may not be injective
> Expected type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
> Actual type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
> Relevant bindings include
> test2 :: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
> (bound at testsuite\Foo.hs:15:1)
> In the expression: Bar
> In an equation for `test2': test2 = Bar
> }}}
> As far as I know, this should compile.
>
> == Example 2 ==
> Another simple example uses
> [https://hackage.haskell.org/package/syntactic syntactic], along with the
> type-family-parameterized GADT:
> {{{#!hs
> {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
>
> module Foo where
>
> import Data.Syntactic
>
> type family PrevElt (xs :: [*]) (a :: *) :: * where
> PrevElt (b ': a ': xs) a = b
> PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
>
> data FooTF :: ((* -> *) -> * -> *) where
> Const :: FooTF prevrp (Full rp)
> Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
>
> type T1 = Double
> type T2 = Float
> type Dom = FooTF (PrevElt '[T1, T2])
>
> leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
> t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
> }}}
>
> By only changing the types `T1` and `T2`:
> {{{#!hs
> {-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
>
> module Foo where
>
> import Data.Syntactic
>
> type family PrevElt (xs :: [*]) (a :: *) :: * where
> PrevElt (b ': a ': xs) a = b
> PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
>
> data FooTF :: ((* -> *) -> * -> *) where
> Const :: FooTF prevrp (Full rp)
> Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
>
> data T
> type T1 = T Double
> type T2 = T Float
> type Dom = FooTF (PrevElt '[T1, T2])
>
> leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
> t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
> }}}
>
> GHC complains:
>
> {{{
> Foo.hs:21:11:
> Couldn't match type ‘Double’ with ‘T Float’
> Expected type: Dom (T1 :-> Full T2)
> Actual type: FooTF T (T Double :-> Full Double)
> In the first argument of ‘inj’, namely
> ‘(Bar :: Dom (T1 :-> Full T2))’
> In the first argument of ‘(:$)’, namely
> ‘inj (Bar :: Dom (T1 :-> Full T2))’
> Failed, modules loaded: none.
> }}}
>
> == Example 3 ==
> I've also attached a larger example (also using
> [https://hackage.haskell.org/package/syntactic syntactic]) that has
> [more, different] errors, which I believe to be related to this problem.
> Errors for the attached file are:
>
> {{{
> Foo.hs:32:6:
> Couldn't match type `NextElt TList (PrevElt ((':) * (T' Float) ('[]
> *)) Double)'
> with `Double'
> Expected type: Double
> Actual type: NextElt TList (PrevElt TList Double)
> In the first argument of `(:$)', namely `inj' Bar'
> In the expression: inj' Bar :$ leaf
> In an equation for `t1': t1 = inj' Bar :$ leaf
>
> Foo.hs:32:11:
> Couldn't match type `PrevElt TList' with T'
> Expected type: Dom (Foo (T' Double) T1 :-> Full (Foo Double T1))
> Actual type: FooTF
> T' (Foo (T' Double) T1 :-> Full (Foo Double T1))
> In the first argument of inj', namely `Bar'
> In the first argument of `(:$)', namely `inj' Bar'
> }}}
>
> In the first error, the `Actual type: NextElt TList (PrevElt TList
> Double)` is strange because `Double` only occurs as a parameter to `T'`,
> and never as a naked type that could be applied to type family.
>
> In the second error, GHC seems to be confusing two types of kind `(* ->
> *)`: `T'` and `PrevElt TList`.
>
> Changing the GADT from type-family-indexed to type-list-index (like in
> the first example) makes the attached code compile. I minimized the
> attached example as much as possible: any changes I made to simplify the
> code resulted in different errors, which may also be helpful for finding
> this bug.
New description:
I seem to have found a dark corner of GHC. In the process of finding a
minimal example, I found a few different ways to trigger a bug. I'm
assuming they are all related.
== Example 1 ==
I started off with a GADT parameterized by a type list:
{{{#!haskell
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
type TList = '[Float, Double]
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooList :: ([*] -> * -> *) where
Bar :: FooList prevrp ((PrevElt prevrp rp) -> rp)
test1 :: FooList TList ((PrevElt TList rp) -> rp)
test1 = Bar
}}}
which compiles as expected.
If I make a syntactic change and parameterize the GADT with the type
family rather than the type list:
{{{#!hs
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
type TList = '[Float, Double]
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Bar :: FooTF prevrp ((prevrp rp) -> rp)
test2 :: FooTF (PrevElt TList) ((PrevElt TList rp) -> rp)
test2 = Bar
}}}
I get a non-sensical error:
{{{
Foo.hs:15:9:
Couldn't match type `PrevElt TList rp' with `PrevElt TList rp'
NB: `PrevElt' is a type function, and may not be injective
Expected type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
Actual type: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
Relevant bindings include
test2 :: FooTF (PrevElt TList) (PrevElt TList rp -> rp)
(bound at testsuite\Foo.hs:15:1)
In the expression: Bar
In an equation for `test2': test2 = Bar
}}}
As far as I know, this should compile.
== Example 2 ==
Another simple example uses [https://hackage.haskell.org/package/syntactic
syntactic], along with the type-family-parameterized GADT:
{{{#!hs
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
import Data.Syntactic
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Const :: FooTF prevrp (Full rp)
Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
type T1 = Double
type T2 = Float
type Dom = FooTF (PrevElt '[T1, T2])
leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
}}}
By only changing the types `T1` and `T2`:
{{{#!hs
{-# LANGUAGE TypeFamilies, GADTs, DataKinds, TypeOperators #-}
module Foo where
import Data.Syntactic
type family PrevElt (xs :: [*]) (a :: *) :: * where
PrevElt (b ': a ': xs) a = b
PrevElt (b ': c ': xs) a = PrevElt (c ': xs) a
data FooTF :: ((* -> *) -> * -> *) where
Const :: FooTF prevrp (Full rp)
Bar :: FooTF prevrp ((prevrp rp) :-> Full rp)
data T a
type T1 = T Double
type T2 = T Float
type Dom = FooTF (PrevElt '[T1, T2])
leaf = inj (Const :: Dom (Full T1)) :: ASTF Dom T1
t1 = inj (Bar :: Dom (T1 :-> Full T2)) :$ leaf :: ASTF Dom T2
}}}
GHC complains:
{{{
Foo.hs:21:11:
Couldn't match type ‘Double’ with ‘T Float’
Expected type: Dom (T1 :-> Full T2)
Actual type: FooTF T (T Double :-> Full Double)
In the first argument of ‘inj’, namely
‘(Bar :: Dom (T1 :-> Full T2))’
In the first argument of ‘(:$)’, namely
‘inj (Bar :: Dom (T1 :-> Full T2))’
Failed, modules loaded: none.
}}}
== Example 3 ==
I've also attached a larger example (also using
[https://hackage.haskell.org/package/syntactic syntactic]) that has [more,
different] errors, which I believe to be related to this problem. Errors
for the attached file are:
{{{
Foo.hs:32:6:
Couldn't match type `NextElt TList (PrevElt ((':) * (T' Float) ('[]
*)) Double)'
with `Double'
Expected type: Double
Actual type: NextElt TList (PrevElt TList Double)
In the first argument of `(:$)', namely `inj' Bar'
In the expression: inj' Bar :$ leaf
In an equation for `t1': t1 = inj' Bar :$ leaf
Foo.hs:32:11:
Couldn't match type `PrevElt TList' with T'
Expected type: Dom (Foo (T' Double) T1 :-> Full (Foo Double T1))
Actual type: FooTF
T' (Foo (T' Double) T1 :-> Full (Foo Double T1))
In the first argument of inj', namely `Bar'
In the first argument of `(:$)', namely `inj' Bar'
}}}
In the first error, the `Actual type: NextElt TList (PrevElt TList
Double)` is strange because `Double` only occurs as a parameter to `T'`,
and never as a naked type that could be applied to type family.
In the second error, GHC seems to be confusing two types of kind `(* ->
*)`: `T'` and `PrevElt TList`.
Changing the GADT from type-family-indexed to type-list-index (like in the
first example) makes the attached code compile. I minimized the attached
example as much as possible: any changes I made to simplify the code
resulted in different errors, which may also be helpful for finding this
bug.
--
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9733#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list