Opened 9 years ago

Closed 5 years ago

#2695 closed bug (fixed)

bogus "syntactically distinct contexts" error

Reported by: conal Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 6.11
Keywords: Cc: conal
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


{-# LANGUAGE TypeOperators, FlexibleContexts
  , MultiParamTypeClasses, FunctionalDependencies
  , TypeFamilies
  -- , ScopedTypeVariables

-- The ScopedTypeVariables is there just as a bug work-around.  Without:
--     Mutually dependent functions have syntactically distinct contexts
--     When matching the contexts of the signatures for
--       dZero :: forall b a s.
--                (AdditiveGroup b, HasBasis a s, HasTrie (Basis a)) =>
--                a :> b
--       pureD :: forall b a s.
--                (AdditiveGroup b, HasBasis a s, HasTrie (Basis a)) =>
--                b -> a :> b
--     The signature contexts in a mutually recursive group should all be identical
--     When generalising the type(s) for dZero, pureD
-- This bug was introduced between ghc 6.9.20080622 and

{-# OPTIONS_GHC -fno-warn-missing-methods #-}

import Control.Applicative

class AdditiveGroup v where
  zeroV   :: v
  (^+^)   :: v -> v -> v
  negateV :: v -> v

class AdditiveGroup v => VectorSpace v s | v -> s where
  (*^)  :: s -> v -> v

-- | Mapping from all elements of @a@ to the results of some function
class HasTrie a where
    data (:->:) a :: * -> *

instance HasTrie a => Functor ((:->:) a)

instance HasTrie a => Applicative ((:->:) a)

class VectorSpace v s => HasBasis v s where
  type Basis v :: *

-- | Linear map, represented a as a memo function from basis to values.
type u :-* v = Basis u :->: v

data a :> b = D { powVal :: b, derivative :: a :-* (a :> b) }

dZero :: (AdditiveGroup b, HasBasis a s, HasTrie (Basis a)) => a:>b
dZero = pureD zeroV

pureD :: (AdditiveGroup b, HasBasis a s, HasTrie (Basis a)) => b -> a:>b
pureD b = b `D` pure dZero

Change History (4)

comment:1 Changed 9 years ago by conal

see also bug #2696

comment:2 Changed 9 years ago by igloo

Component: CompilerCompiler (Type checker)
difficulty: Unknown
Milestone: 6.10.2

Thanks for the report

comment:3 Changed 9 years ago by simonpj

Milestone: 6.10.2_|_
Priority: normallow

Good point. The requirement that the contexts of all the declarations in a mutually recursive group must be identical, even though really we have polymorphic recursion, is a very tiresome Haskell 98 thing. What is biting us here is that we're trying to unify the two contexts, but since Basis is a type function, knowing that (Basis a1) = (Basis a2) does not allow us to conclude that a1 = a2.

We could solve this by writing a syntactic-identity checker (oh, but it has to be subject to alpha-renaming...), but it just doesn't seem worth the bother.

The solution is to use -XRelaxedPolyRec, which lifts the restriction altogether. Haskell Prime will probably have this as the default.

Meanwhile I'll leave this open at low priority.


comment:4 Changed 5 years ago by monoidal

Resolution: fixed
Status: newclosed
Type of failure: None/Unknown

As of GHC 7.6, the code compiles fine. -XRelaxedPolyRec is the default and cannot be switched off.

Note: See TracTickets for help on using tickets.